Semantyka i weryfikacja programów 2014/15.
Zadanie 3.
Język Tiny
Anad 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|
Array= Int→Int,
a operacje interpretowane są jako funkcje newarr
A: |A|
Arrayput
A: |A|
Array× |A|
Int× |A|
Int→ |A|
Arrayget
A: |A|
Array× |A|
Int→ |A|
Intswap
A: |A|
Array× |A|
Int× |A|
Int→ |A|
Arrayzdefiniowane następująco:
newarr
A(i) = 0
put
A(a, i, n) = a[i 7→ n]
get
A(a, i) = a(i)
swap
A(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 γ
1, γ
2i γ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)]