put : Array × Int × Int → Array get : Array × Int → Int

Semantyka i weryfikacja programów 2014/15.

Zadanie 3.

Język Tiny

nad typem danych rozszerzonym o rodzaj Array i operacje newarr : Array

put : Array × Int × Int → Array get : Array × Int → Int

swap : Array × Int × Int → Array

Nośnik rodzaju Array to zbiór funkcji (całkowitych) z liczb całkowitych w liczby całkowite,

|A|

= Int→Int,

a operacje interpretowane są jako funkcje newarr

: |A|

put

: |A|

× |A|

× |A|

→ |A|

get

: |A|

× |A|

→ |A|

swap

: |A|

× |A|

× |A|

→ |A|

zdefiniowane następująco:

newarr

(i) = 0

put

(a, i, n) = a[i 7→ n]

get

(a, i) = a(i)

swap

(a, i, j) = a[i 7→ a(j), j 7→ a(i)]

dla wszystkich i, j, n ∈ Int i a : Int→Int.

Ponadto, w asercjach wykorzystujemy „predykat” a:Array stwierdzajacy, że zmienna a jest rodzaju Array (pozostałe zmienne są rodzaju Int ).

Poniżej dany jest program w tym języku. Należy udowodnić całkowitą poprawność tego pro- gramu względem podanych warunków. Wymagane jest podanie niezmienników γ

, γ

i γ3 pętli programu, związanych z tymi pętlami adnotacji dla dowodzenia własności stopu oraz asercji pośrednich α1,...,α5.

Do celów specyfikacji wprowadzamy predykaty:

S

(a, i, j) ≡ a : Array ∧ ∀p.i ≤ p < j ⇒ get(a, p) ≤ get(a, p + 1)

In(X, i, Y, j) ≡ X : Array∧Y : Array∧∀p.1 ≤ p ≤ i ⇒ (∃q.1 ≤ q ≤ j ∧get(X, p) = get(Y, q))

1

[1≤n ∧ 1≤m ∧ a:array ∧ b:array ∧ c:array ∧S⁺(a,1,n) ∧S⁺(b,1,m)]

[ ]

i:=1;

j:=1;

k:=1;

[ ]

while [γ1:S⁺(a,1,n) ∧S⁺(b,1,m) ∧S⁺(c,1,k-1) ∧ 1≤i≤n+1 ∧ 1≤j≤m+1 ∧ k=i+j-1 ∧ (k>1⇒ (i≤n ⇒get(c,k-1)≤ get(a,i)) ∧ (j≤m ⇒get(c,k-1)≤get(b,j))) ∧

In(a,i-1,c,k-1) ∧ In(b,j-1,c,k-1)]

(i≤n) and (j≤m) do [decr m+n+1-k in Nat wrt < ] [γ1 ∧ (i≤n) ∧ (j≤m) ]

(

[S⁺(a,1,n)∧S⁺(b,1,m)∧ 1≤i+1≤n+1∧ 1≤j≤m+1∧ k=i+j-1∧ (get(a,i)≤ get(b,j)∧

S⁺(put(c,k,get(a,i)),1,k)∧ In(a,i,put(c,k,get(a,i)),k)∧ In(b,j-1,put(c,k,get(a,i)),k)

∨ get(a,i)>get(b,j) ∧S⁺(put(c,k,get(b,j)),1,k)∧ In(a,i-1,put(c,k,get(b,j)),k)

∧ In(b,j,put(c,k,get(b,j)),k))]

if get(a,i)≤ get(b,j) then (

[α1:S⁺(a,1,n)∧S⁺(b,1,m)∧S⁺(put(c,k,get(a,i)),1,k)∧ 1≤i+1≤n+1∧ 1≤j≤m+1∧ k=i+j-1∧

(j≤m ⇒get(a,i)≤get(b,j))∧ In(a,i,put(c,k,get(a,i)),k)∧ In(b,j-1,put(c,k,get(a,i)),k)]

c:=put(c,k,get(a,i));

i:=i+1 )

else (

[α2:S⁺(a,1,n)∧S⁺(b,1,m)∧S⁺(put(c,k,get(b,j)),1,k)∧ 1≤i≤n+1∧ 1≤j+1≤m+1∧ k=i+j-1∧

(i≤n ⇒get(b,j)≤ get(a,i))∧ In(a,i-1,put(c,k,get(b,j)),k)∧ In(b,j,put(c,k,get(b,j)),k)]

c:=put(c,k,get(b,j));

j:=j+1 );

[α3:S⁺(a,1,n)∧S⁺(b,1,m)∧S⁺(c,1,k)∧ 1≤i≤n+1∧ 1≤j≤m+1∧ k=i+j-2∧

(k+1>1⇒(i≤n ⇒get(c,k)≤ get(a,i))∧ (j≤m ⇒get(c,k)≤get(b,j)))∧

In(a,i-1,c,k) ∧ In(b,j-1,c,k)]

k:=k+1 );

[α4: (i=n+1 ∨ j=m+1) ∧γ1 ] while [γ2: (i=n+1 ∨ j=m+1) ∧γ1 ]

i≤n do[ decr n+1-i in Nat wrt < ] [i≤n ∧ j=m+1 ∧γ1]

(

[i=n+1 ∨ j=m+1)∧S⁺(a,1,n) ∧S⁺(b,1,m)∧S⁺(put(c,k,get(a,i),1,k)∧ 1≤i+1≤n+1∧

1≤j≤m+1∧ k=i+j-1∧ (j≤m ⇒(a,i)≤get(b,j))∧

In(a,i,put(c,k,get(a,i),k)∧ In(b,j-1,put(c,k,get(a,i),k) ] c:=put(c,k,get(a,i));

[(i=n+1 ∨ j=m+1)∧S⁺(a,1,n) ∧S⁺(b,1,m) ∧S⁺(c,1,k) ∧ 1≤i+1≤n+1 ∧ 1≤j≤m+1 ∧ k=i+j-1 ∧ (i+1≤n ⇒get(c,k)≤ get(a,i+1)) ∧ (j≤m ⇒get(c,k)≤get(b,j)) ∧ In(a,i,c,k) ∧ In(b,j-1,c,k)]

i:=i+1;

k:=k+1;

);

[α5: i=n+1 ∧γ1 ]

while [γ3(=α5):i=n+1 ∧S⁺(a,1,n) ∧S⁺(b,1,m) ∧S⁺(c,1,k-1) ∧ 1≤j≤m+1 ∧ k=i+j-1 ∧ (j≤m ⇒get(c,k-1)≤get(b,j)) ∧ In(a,n,c,k-1) ∧ In(b,j-1,c,k-1) ]

j≤m do [decr m+1-j in Nat wrt < ] [ γ3 ∧ j≤m ]

(

[i=n+1 ∧S⁺(a,1,n)∧S⁺(b,1,m)∧S⁺(put(c,k,get(b,j)),1,k)∧ 1≤j+1≤m+1 ∧ k=i+j-1∧

∧ In(a,n,put(c,k,get(b,j)),k)∧ In(b,j,put(c,k,get(b,j)),k)]

c:=put(c,k,get(b,j));

2

[i=n+1 ∧S⁺(a,1,n)∧S⁺(b,1,m)∧S⁺(c,1,k)∧ 1≤j+1≤m+1 ∧ k=i+j-1∧

(j+1≤m ⇒get(c,k)≤get(b,j+1))∧ In(a,n,c,k)∧ In(b,j,c,k)]

j:=j+1;

k:=k+1;

[i=n+1 ∧ S⁺(a,1,n) ∧S⁺(b,1,m) ∧S⁺(c,1,k-1) ∧ 1≤j≤m+1 ∧ k=i+j-1 ∧ (j≤m ⇒get(c,k-1)≤get(b,j)) ∧ In(a,n,c,k-1) ∧ In(b,j-1,c,k-1)]

);

[i=n+1 ∧ j=m+1 ∧ γ3 ]

[i=n+1 ∧ j=m+1 ∧ S⁺(a,1,n) ∧S⁺(b,1,m) ∧S⁺(c,1,k-1) ∧ k=i+j-1 ∧ In(a,n,c,k-1) ∧ In(b,m,c,k-1)]

[S⁺(c,1,n+m) ∧ In(a,n,c,n+m) ∧ In(b,m,c,n+m)]

3