1673068215

12 Wykład 15.04.2008

12.1    Wprowadzenie

Mamy l= 2 + 2 = 4, ale często wystarcza i- 2 + 2 = 4 (bo arytmetyka nie musi być wcale „taka skomplikowana”) do weryfikowania poprawności programów.

Definicja.

• i- {<p}c{ip} => f= {ip}c{ip}    - mówimy, że taki system jest adekwatny

• ^ {¥’}^C{V’} =*■ i- {<p}c{?/j}    - mówimy, że taki system jest zupełny Ale z zupełnością jest pewien problem¹.

Weźmy sobie nasz imperatywny język: a ::= n | X \ a © a © ::= + | - | x | div | mod b ::= a\ ©    | ->&1 6i ® i>2

© ::= A | V | ^ | <=>

© ::= < | > | S | i | = | *

c ::= skip | abort | X := a | if b then c\ else C2 | if b then c | while b do c | ci; C2

Można dołożyć asercje do języka - każda instrukcja w tym języku będzie miała „z przodu” i „z tyłu” jakieś asercje:

c ::= {<£>} skip {tp} |... | {ip} if b then {<p^;} c {<p^w} ; {ip}

| {<p} while 6 do {ip'} c {y>"} ; {ip}

I M oi; W <!2 {«}

I MM} c W}

I Mc W W>

W Haskellu mamy rekonstrukcję typów² - zatem nie wszędzie musimy pisać typy. Są jednak miejsca, gdzie takie typy trzeba napisać (bo rekonstrukcja typów jest czasami nierozstrzygalna, ale weryfikacja poprawności już tak - nawet liniowa).

12.2    Asercje

Problem z dowodzeniem poprawności programów polega na tym, że tablica może być za mała... Popatrzmy na taki programik obliczający silnię:

1 I* {X = n}

2    S := 1

3    while X * 1 do

4    S    :=    X x    S;

s    X    :=    X -    1;

6    done

7    *    {5 = 7l!}

19

1

mamy np. niezupełność arytmetyki

2

system typów Haskella jest dużo bardziej skomplikowany niż w SMLu