Gruppe 09 (Enrico Göhrs, Christian Langolf)

Arbeitsblatt 2.1
<a -> 6, c -> 2>

A: Ja
B: Nein
C: Nein
D: Ja

A: <x -> 1, a -> 3, y -> 1>
B: <x -> 3, a -> 3>
C: <x -> 4, y -> 1, a -> 3>

1: True
2: False, x == 6
3: False, x == 6
4: False, x ist undefiniert
5: False, x ist undefiniert
6: False, x == 2

<x -> 5, y -> 2>
while(y != 0) <y != 0, <x -> 5, y -> 2>> -> Bexp true
x = x * x;
<x -> 25, y -> 2>
y = y - 1;
<x -> 25, y -> 1>
while(y != 0) <y != 0, <x -> 25, y -> 1>> -> Bexp true
x = x * x;
<x -> 625, y -> 1>
y = y - 1;
<x -> 625, y -> 0>
while(y != 0) <y != 0, <x -> 25, y -> 0>> -> Bexp false
<x -> 625, y -> 0>

3.1

sqrt(x) = y g.d.w. y^2=x
sqrt = {(0,0),(1,1),(4,2),(9,3),(16,4),(25,5),(36,6),(49,7),(64,8),(81,9),(100,10)}

t_1 = 5-sqrt(32) = 5- undef. = undef
t_2 = sqrt(49) - sqrt(0) = 7-0 = 7
t_3 = Sqrt(3) * sqrt(3) = undef * undef = undef
t_4 = sqrt(64)/0 = 8/0 = undef

3.2

(s,7)
(s,7)
(s,21)
(s,4)
(s,25)

[[7x+y]](s) = [[7x]](s)+[[y]](s) = [[7]](s)[[x]](s)+[[y]](s) = 73+4 = 21+4 = 25

Blatt 3.4

R ° S = {(1,3),(2,1),(3,?),(4,1)}

s G^0 G^1 G^2 G^3 G^4
n x n x n x n x n x n
0 \bot 1 0 1 0 1 0 1 0
1 \bot \bot 1 0 1 0 1 0
2 \bot \bot \bot 2 0 2 0
3 \bot \bot \bot \bot 6 0

4.2

4.3
Annahme:
<a1, o> -> Aexp n <=> (o, n) elem [[a1]]B
<a2, o> -> Aexp m <=> (o, m) elem [[a1]]B

Fälle:
n = true
n = false
~~(Im Grunde genommen ist das dasselbe wie &&, also analog zu b1 && b2)~~ Das eine ist arithmetisch, das andere boolsch

5.1
Was berechnet das Programm: 2^y
Eingangsvariable: y
Ausgangsvariable: x
Arbeitsvariable: c

(A): y >= 0
(B): y >= 0, x=c=1
©: c <= y
(D): c ist um 1 größer als bei ©,
(E): x = 2^y

5.2

      I1     I2     I3
     p q a  p q a  p q a
s1   T F F  F T T  F T T
s2   F F T  T T T  F T T
s3   F F T  F F T  T T T

a = 2*x=X --> x<=X

5.3

Gilt, da die if-Anweisung durch die Vorbedingung x>=3 nie ausgeführt wird
Gilt nicht, da b != B in der Anweisung x = a+b
Gilt

5.4

A) {p=c!}
B) {p=(c-1)!}

5.5

C) {y = X and x - y = Y}
B) {x - y = X and y = Y}
A) {x = X and y = Y}

5.6

//F) {true}
if(x < y)
    // E) {x < y and true}
    // {x <= y}
    // {true and x <= y and (true or x = y)}
    // {x <= x and x <= y and (x = x or x = y)}
    z = x;
    // C) {z <= x and z <= y and (z = x or z = y)}
else
    // D) {!(x < y) and true}
    // {y <= x and true and (y = x or true)}
    // {y <= x and y <= y and (y = x or y = y)}
    z = y;
    // B) {z <= x and z <= y and (z = x or z = y)}
// A) {z <= x and z <= y and (z = x or z = y)}

6.1

// {0 <= n}
x = 0;
c = 1;
//
while(c <= n) {
    // {I}
    x = x + c;
    c = c + 1;
    // {I}
}
//
// {x = sum(0,n)}

1. Invariante: I := {x = sum(0, c-1) and c - 1 <= n}
2. c - 1 <= n und !(c <= n), da so c - 1 = n
3. ?

6.2

// {n = N and 0 <= n} />
x = 0;
// {I}
while (n != 0) {
    x = x+n;
    n = n-1;
    // {I}
}
// {I}
// {x = sum(0, N)}

Invariante I:= x = sum(n + 1, N)

/>/>

Blatt 4 bearbeitung:

a)
```
// { x= c* m }
// { x + m = (c + 1 - 1) * m + m}
// { x + m = (c + 1) * m}
x= x+ m;
// { x= (c + 1) * m }
c= c+1;
// { x= c* m }
```

b)
```
// { x= (c-1)* m }
// { x + m = (c - 1) * m + m}
// { x + m = (((c + 1) - 1) - 1) * m + m}
// { x + m = ((c + 1) - 1) * m}
x= x+ m;
// { x= ((c + 1) - 1) * m}
c= c+1;
// { x= (c-1)* m }
```

4.2
PRE = `{ x = X and y = Y }`
POST = `{ x <= y and ((X <= Y and x = X and y = Y) or (X > Y and x = Y and y = X))}`/>/>

// (PRE) = { (x = X and y = Y) or (x = Y and y = X) }
// 
if (y <= x) {
  // { y <= x and ((y = X and x = Y) or (y = Y and x = X))}
  z= y;
  // { z <= x and ((z = X and x = Y) or (z = Y and x = X))}
  y= x;
  // { z <= y and ((z = X and y = Y) or (z = Y and y = X))}
  x= z;
  // { x <= y and ((x = X and y = Y) or (x = Y and y = X))}
  }
else {
  // { x <= y and ((x = X and y = Y) or (x = Y and y = X))}
  }
// 
// (POST) = { x <= y and ((x = X and y = Y) or (x = Y and y = X))}
       
Korrektur:
PRE = (x = X and y = Y)
if (y < x) {
    z = y;
    y = x;
    x = z;
} else {
    // {x = X and y = Y and not(y <= X)}
    // {x < y and (x = X and y = Y)}
    // {x < y and ((x = X and y = Y) oder (x = Y and y = X))}
}
POST = {x < y and ((x = X and y = Y) oder (x = Y and y = X))}

6.3

// {0 <= a}
r=a;
q=0;
while(b<=r) {
    // {a = b * q + r and 0 <= (r - b)}
    // {a = b * q + b + r - b and 0 <= (r - b)}
    // {a = b * q + b + r and 0 <= r}
    r=r-b;
    // {a = b * q + b + r and 0 <= r}
    // {a = b * (q + 1) + r and 0 <= r}
    q=q+1;
    // {a = b * q + r and 0 <= r}
}
// {a = b * q + r and 0 <= r and not(b <= r)}
// {a = b * q + r and 0 <= r and r < b}

Übung 5

PRE = { n >= c and c = 1 and x = 0 }
c und x kommen nicht in die Vorbedingung, weil diese erst im Abschnitt
definiert werden. Was die davor haben ist für uns nicht relevant
Daher eher PRE = { n >= c }
POST = {c <= n and x = n * c? }
Ist das nicht eher x = n * m? Weil mit jedem Durchlauf wird m aufaddiert
und dies wird n mal durchgeführt
Und c <= n kann nicht in der Nachbedingung stehen, da man ansonsten noch innerhalb der While-Schleife wäre

PRE = { n >= 0 }
POST = { x = n * m and c > n}
             
// (PRE)
// { 0 <= n }
// { 0 = 0 and 0 <= n }
x= 0;
// { x = 0 and 0 <= n }
// { x = 0 * m and 0 <= n }
// { x = (1 - 1) * m and (1 - 1) <= n }
c= 1;
// { x = (c - 1) * m and (c - 1) <= n }
while (c <= n) {
  // { x = (c - 1) * m and (c - 1) <= n } //Weakening. Wenn c <= n, dann auch c - 1 <= n
  // { x + m = (c - 1) * m + m and c <= n }
  // { x + m = c * m and c <= n }
  x= x+ m;
  // { x = c * m and c <= n }
  // { x = (c + 1) - 1 * m and (c + 1) - 1 <= n }
  c= c+1;
  // { x = (c - 1) * m and c - 1 <= n }
}
// Invariante: {x = (c - 1) * m and c - 1 <= n }
// {x = n * m and c > n}

// (POST)

7.1

o |=' (a0 = a1)[e/x] <=> o |=' (a0[e/x] = a1[e/x])
o |=' (a0 = a1)[e/x] <=> o |=' [[a0[e/x]]]'A(o) = [[a1[e/x]]]'A(o)
o |=' (a0 = a1)[e/x] <=> o |=' [[a0]'A(o[x->[[e]]'A(o)) = [[a1]'A(o[x->[[e]]'A(o))

Fälle:
 - Falls o[x -> [[e]]'A(o)] undefiniert
    Dann ist recht _|_ = _|_ was selvst wieder _|_ ist, also undefiniert. Also ist o |= (a0 = a1)[e/x] undefiniert
    Gleichzeitig ist [[a0 = a1]]'B(o[x -> [[e]]'A()])

 - Falls o[x -> [[e]]'A(o)] definiert
    [[a0 = a1]]'B(o[x->[[e]]'A(o)]) = true wenn [[a0]]'A(o[x->[[e]]'A(o)]) = [[a1]]'A(o[x->[[e]]'A(o)])
    sonst false

8.1

int a[2];
int b[2];
// {0 <= n and 0 <= m and n <= m}
// {true}
// {m^2 - n^2 = m^2 - n^2}
// {(m - n) * (m + n) = m^2 - n^2}
a[0] = m;
// {(a[0] - n) * (a[0] + n) = m^2 - n^2}
b[0] = a[0] - n;
// {b[0] * (a[0] + n) = m^2 - n^2}
b[1] = a[0] + n;
// {b[0] * b[1] = m^2 - n^2}
a[1] = b[0] * b[1];
// {a[1] = m^2 - n^2}

------------------------
                                
int a[3]; 
int i;
// {0 ≤ n}
// {(3 * n = 3 * n)
// {(2 = 2 and 3 * n = 3 * n) or (2 != 2 and a[2] * n = 3 * n)}
i=2;
// {(i = 2 and 3 * n = 3 * n) or (i != 2 and a[2] * n = 3 * n)}
a[i] = 3;
// {a[2] * n = 3 * n}
a[0] = n;
// {a[2] * a[0] = 3 * n}
a[2] = a[2] ∗ a[0];
// {a[2] = 3 ∗ n}

9.1

// (?) { (3 + y == 10 && y == 7) || (10 + 0 == 10 && y != 7) }
if ( y == 7 ) {
    // (A) { 3 + y == 10 && y == 7 }
    x= 3 ;
    // { x + y == 10 }
}
else {
    // (B) { 10 + 0 == 10 && y != 7 }
    y= 0 ;
    x= 10;
    // { x + y == 10 }
}
// { x+ y == 10 }

9.2

A = (P1 && b) || (P2 && !b)

(1) A && b ==> P1
(2) A && !b ==> P2

A && b ==> P1
((P1 && b) || (P2 && !b)) && b ==> P1
(P1 && b && b) || (P2 && !b && b) ==> P1
(P1 && b) || (P2 && False) ==> P1
(P1 && b) || False ==> P1
P1 && b ==> P1

A && !b ==> P2
((P1 && b) || (P2 && !b)) && !b ==> P2
(P1 && b && !b) || (P2 && !b && !b) ==> P2
(P1 && False) || (P2 && !b) ==> P2
False || (P2 && !b) ==> P2
P2 && !b ==> P2

7.1: Summ, summ, summ …

Das annotierte Programm:

// { 0 <= n } 
// { 0 = 0 && 0 >= 0 && 0 <= n }
// { 0 = array_sum(a, 0, 0 - 1) && 0 >= 0 && 0 <= n }
i= 0;
// { 0 = array_sum(a, 0, i - 1) && i >= 0 && i <= n }
s= 0;
// { s = array_sum(a, 0, i - 1) && i >= 0 && i <= n }
while (i < n) {
  // { s = array_sum(a, 0, i - 1) && i >= 0 && i <= n && i < n }
  // { s = array_sum(a, 0, i - 1) && (i - 1) + 1 >= 0 && (i - 1) + 1 <= n && (i - 1) + 1 < n }
  // { s + a[i] = array_sum(a, 0, i) && i + 1 >= 0 && i + 1 <= n && i + 1 < n }
  s= s+ a[i];
  // { s = array_sum(a, 0, i) && i + 1 >= 0 && i + 1 <= n && i + 1 < n }
  // { s = array_sum(a, 0, (i + 1) - 1) && i + 1 >= 0 && i + 1 <= n && i + 1 < n }
  i= i+1;
  // { s = array_sum(a, 0, i - 1) && i >= 0 && i <= n && i < n }
  }
// { s = array_sum(a, 0, i - 1) && i <= 0 && i <= n && !(i < n) } 
// { s = array_sum(a, 0, n-1) }

9.3

// { 0 <= n && n = N }
// { 0 = sum(n + 1, N) }
p = 0
// { p = sum(n + 1, N) }
while (n > 0) //** inv p = sum(n + 1, N); */
{
// { p + n = sum((n - 1) + 1, N) }
    p = p + n
// { p = sum((n - 1) + 1, N)}
    n = n - 1
// { p = sum(n + 1, N)}
}
// { p = sum(1,N) }

1| p = sum(n + 1, N) && !(n > 0) --> p = sum(1,N)
2| p = sum(n + 1, N) && 0 < n --> p + n = sum(n,N)
3| 0 <= n && n = N --> 0 = sum(n+1,N)

9.5

i = 0;
while (i < m)
{
    b[m - 1 - i] = a[i];
    i = i + 1;
}
// 
// b[i] = a[m - 1 - i]

10.2

$\exists x.x < 7$ TRUE (x == 6)
$\exists y \exists x.x + 3 = y$ TRUE (x == 0, y == 3)
$\exists x.x < 3 \land x > 7$ FALSE (x kann nicht kleiner 3 und gleichzeitig größer 7 sein)
$\forall x \exists y.x \cdot y = 3$ FALSE (x == 2 => y müsste 1.5 sein, was aber nicht in Z ist)
$\exists x.x < 7 \lor x < 3$ TRUE (x == 2)
$\exists x \forall y.x \cdot y = y$ TRUE (x == 1)

Arbeitsblatt 8.1

// {0 < a \And 0 < b \And a = A \And b = B} 
// { ggt(a,b) = ggt(A,B) }
while (b != 0) /** inv {ggt(a,b) = ggt(A,B)} */
{
  // {  }
  // { (a <= b && ggt(a, b-a) = ggt(A,B)) || (!(a <= b) && ggt(a-b,b) = ggt(A,B)) }
  if (a <= b) {
    // { ggt(a, b-a) = ggt(A,B)}
    b = b - a;  
    // { ggt(a,b) = ggt(A,B) }
    }
  else {
    // { ggt(a-b,b) = ggt(A,B) }
    a = a - b;
    // { ggt(a,b) = ggt(A,B) }
    }
  // { ggt(a,b) = ggt(A,B) }
}
// {a= ggt(A, B)}

1 | ggt(a,b) = ggt(A,B) && !(a <= b) --> a = ggt(A,B)
2 | ggt(a,b) = ggt(A,B) && a <= b --> (a <= b && ggt(a, b-a) = ggt(A,B)) || (!(a <= b) && ggt(a-b, b) = ggt(A,B))
3 | 0 < a && 0 < b && a = A && b = B --> ggt(a,b) = ggt(A,B)

1 | ggt(a,b) = ggt(A,B) && b < a --> a = ggt(A,B)
2 | ggt(a,b) = ggt(A,B) && a <= b --> (a <= b && ggt(a,b) = ggt(A,B)) || (b < a && ggt(a,b) = ggt(A,B))
3 | 0 < a && 0 < b && a = A && b = B --> ggt(a,b) = ggt(A,B)

// {0 < a \And 0 < b \And a = A \And b = B} 
// { ggt(a,b) = ggt(A,B) }
while (b != 0) /** inv {ggt(a,b) = ggt(A,B)} */
{
  // {  }
  // { (a <= b && ggt(a, b-a) = ggt(A,B)) || (!(a <= b) && ggt(a-b,b) = ggt(A,B)) }
  if (a <= b) {
    // { ggt(a, b-a) = ggt(A,B)}
    b = b - a;  
    // { ggt(a,b) = ggt(A,B) }
    }
  else {
    // { ggt(a-b,b) = ggt(A,B) }
    a = a - b;
    // { ggt(a,b) = ggt(A,B) }
    }
  // { ggt(a,b) = ggt(A,B) }
}
// {a= ggt(A, B)}

Verifikationsbedingungen

Vereinfachten Verifikationsbedingungen

Die initialen Beweisverpflichtungen:

…

Die vereinfachten Beweisverpflichtungen, mit Angabe einer Beweiskizze (welches Theorem wird benutzt, s. Vorlesung).

…

10.3: Vorwärtsverkettung

// {x = X and y = Y}
x = x + y
// { $\exists A. (x = X \land y = Y)[A/x] \land x = x + y[A/x]$ }
// { $\exists A. A = X \land y = Y \land x = A + y$ }
y = x - y
// { $\exists B. (\exists A. A = X \land y = Y \land x = A + y)[B/y] \land y = (x - y)[B/y]$ }
// { $\exists B. (\exists A. A = X \land B = Y \land x = A + B) \land y = (x - B)$ }
// { $\exists B. \exists A. A = X \land B = Y \land x = A + B \land y = x - B$ }
x = x - y
// { $\exists C. (\exists B. \exists A. A = X \land B = Y \land x = A + B \land y = x - B)[C/x] \land x = (x - y)[C/x]$ }
// { $\exists C. (\exists B. \exists A. A = X \land B = Y \land C = A + B \land y = C - B) \land x = (C - y)$ }
// { $\exists C. \exists B. \exists A. A = X \land B = Y \land C = A + B \land y = C - B \land x = C - y$ }

Es verstauscht x und y
x = Y und y = X

10.4:

/** {0 <= a } /
r = a;
// { $\exists R. (0 <= a)[R/r] \land r = a[R/r]$ }
// { $\exists R. 0 <= a \land r = a$ }
// { $0 <= a \land r = a$ }
q = 0;
// { $\exists Q. (0 <= a \land r = a)[Q/q] \land q = 0[Q/q]$ }
// { $\exists Q. 0 <= a \land r = a \land q = 0$ }
// { $0 <= a \land r = a \land q = 0$ }
while (b <= r) /** inv { a == bq+r && 0 <= r } * / {
r = r-b;
// { $\exists V1. (a == b*q+r \land 0 <= r)[V1/r] \land r = (r-b)[V1/r]$ }
// { $\exists V1. a == b*q+V1 \land 0 <= V1 \land r = V1-b$ }
q = q+1;
// { $\exists V2. (\exists V1. a == b*q+V1 \land 0 <= V1 \land r = V1-b)[V2/q] \land q = (q+1)[V2/q]$ }
// { $\exists V2. \exists V1. a == b*V2+V1 \land 0 <= V1 \land r = V1-b \land q = V2+1$ }
}
// { $\lnot (b <= r) \land a == b*q*r \land 0 <= r$ }
/**** { $a == b * q + r \land 0 <= r \land r < b$ } */

$VC_1$ = { $0 <= a \land r = a \land q = 0 --> a == b*q+r \land 0 <= r$ }
$VC_2$ = { $0 <= a \land r = a \land q = 0 --> a == b*q+r \land 0 <= r \cup \exists V2. \exists V1. a == b*V2+V1 \land 0 <= V1 \land r = V1-b \land q = V2+1 --> \exists V2. \exists V1. a == b*V2+V1 \land 0 <= V1 \land r = V1-b \land q = V2+1$ }

11.1:

$f = {(0,0), (1,0), (2,1), (3,100), (4,3), (5,4), (6,200), (7,6), (8,7), (9,300)}$
$f_2 = {(0, 0), (1, 0), (2, 0), (3, 100), (4, 100), (5, 3), (6, 200), (7, 200), (8, 6), (9, 300)}$
$f_3 = {(0, 0), (1, 0), (2, 0), (3, 100), (4, 100), (5, 100), (6, 200), (7, 200), (8, 200), (9, 300)}$

11.2

$[[x = 3; x= 4]]c = [[x=4]]c \circ [[x = 3]]$
= ${(o', o'[x \implies 4]) \circ {o, o[x \implies 3]}}$
[[x = 3; return x; x= 4]]c = ?

11.3

{   // { x = X }
    // { x + 1 = X + 1 }
    x = x+1
    // { x = X + 1 }
    return x;
    // { false | \result == X + 1}
}

Beweisverpflichtung:
$x = X \implies x + 1 = X + 1$

9. Übungsblatt

9.1 Immer Was Drauf

Vor- und Nachbedingung:
PRE = { $n >= 0 \land c = C \land a = A$ }
POST = { $\forall x. 0 <= x < n \implies a[x] = A[x] + C$ }
Komplett annotiertes Programm:
// { PRE }
// { $n >= 0 \land c = C \land a = A$ }
i = 0;
// { $\forall I. (n >= 0 \land c = C \land a = A)[I/i] \land i = 0[I/i]$ }
// { $n >= 0 \land c = C \land a = A \land i = 0$ }
while (i < n) { /* inv $\forall x. 0 <= x < i \implies a[x] = A[x] + c$ */
a[i] = a[i] + c;
// { $\forall V1. (\forall x. 0 <= x < i \implies a[x] = A[x] + c)[V1/a[i]] \land a[i] = (a[i] + c)[V1/a[i]]$ }
// { $\forall V1. \forall x. 0 <= x < i \implies a[x] = A[x] + c \land a[i] = V1 + c$ }
i = i + 1;
// { $\forall V2. (\forall V1. \forall x. 0 <= x < i \implies a[x] = A[x] + c \land a[i] = V1 + c)[V2/i] \land i = (i + 1)[V2/i]$ }
// { $\forall V2. \forall V1. \forall x. 0 <= x < V2 \implies a[x] = A[x] + c \land a[V2] = V1 + c \land i = V2 + 1$ }
// { $\forall V2. \forall V1. \forall x. 0 <= x < V2 \implies a[x] = A[x] + c \land a[V2] = V1 + c \land V2 = i - 1$ }
// { $\forall V1. \forall x. 0 <= x < i - 1 \implies a[x] = A[x] + c \land V1 = a[i - 1] - c$ }
// { $\forall x. 0 <= x < i - 1 \implies a[x] = A[x] + c$ }

}
// { $\forall x. 0 <= x < i \implies a[x] = A[x] + c \land \lnot(i < n)$ }
// { $\forall x. 0 <= x < n \implies a[x] = A[x] + C$ }

Berechnete Verifikationsbedingungen:
1 | $n >= 0 \land c = C \land a = A \land i = 0 \implies \forall x. 0 <= x < i \implies a[x] = a[x] + C$
2 | $\forall x. 0 <= x < i \implies a[x] = A[x] + c \implies \forall x. 0 <= x < i - 1 \implies a[x] = A[x] + c$
Vereinfachte Verifikationsbedingungen:
1.1 | $n >= 0 \land c = C \land a = A \land i = 0 \implies
Beweisskizzen für nicht-triviale Verifikationsbedingungen:
svc = {{asp \implies \forall x. 0 <= x < n \implies a[x] = A[x] + C$ } = \forall x. 0 <= x < i \implies a[x] = A[x] + c \land \lnot(i < n), }

12.1

C: Bei C kann es definiert werden, ob eine Referenz, ein Pointer oder lediglich der Wert übergeben wird.
Java: Bei Immutable Objects (Primitive Datentypen wie Int, Char, String) ist es Call-by-value, bei anderen Datenobjekten Call-by-reference
Haskell: Ausschließlich Call-by-value
Python: Wie bei Java Call-by-value bei immutable Objects, ansonsten Call-by-reference

10. Übungsblatt

Gruppe

Name: Enrico Göhrs
Matrikel-Nr: 4580450

Christian Langolf
Matrikel-Nr: 4578221

Name:
Matrikel-Nr:

10.1: Größer gemeinsamer Teiler (Reprise)

10.1.(i):

pre = $0 \leq a \land 0 \leq b$

post = \result $= ggT(a, b)$
oder
post = \result $a == b$

10.1.(ii):

inv = $0 \leq ggT(a, b)?$ k.A xD

10.1.(iii):

Annotiertes Programm mit schwächsten Vorbedingungen:

int ggt(int a, int b)
/** pre: {0 < a \And 0 < b \And a = A \And b = B}
    post: \result = ggT(a, b)
*/
{
  // { 0 <= ggT(a, b) }
  while (1) /** inv { ggt(a,b) = ggt(A,B) } */ {
    // { (a <= b && ggt(a, b-a) = ggt(A,B)) || (!(a <= b) && ggt(a-b,b) = ggt(A,B)) || a = ggT(a, b) }
    if (a == b) {
      // {a = ggT(a, b)}
      return a;
      // {{ (a <= b && ggt(a, b-a) = ggt(A,B)) || (!(a <= b) && ggt(a-b,b) = ggt(A,B)) } || \result = ggT(a, b)}
      }
    else {
      // { (a <= b && ggt(a, b-a) = ggt(A,B)) || (!(a <= b) && ggt(a-b,b) = ggt(A,B)) }
      }
    // { (a <= b && ggt(a, b-a) = ggt(A,B)) || (!(a <= b) && ggt(a-b,b) = ggt(A,B)) }
    if (a <= b) {
      // { ggt(a,b-a) = ggt(A,B) }
      b= b- a;
      // { ggt(a,b) = ggt(A,B) }
      }
    else {
      // { ggt(a-b,b)) = ggt(A,B) }
      a= a-b;
      // { ggt(a,b) = ggt(A,B) }
      }
    // { ggt(a,b) = ggt(A,B) }
    }
}

Berechnete Verifikationsbedingungen:
1 | $ggt(a,b) = $ggt(A,B) \land true --> (a <= b && ggt(a, b-a) = ggt(A,B)) || (!(a <= b) && ggt(a-b,b) = ggt(A,B)) || a = ggT(a, b)$
2 | $0 < a \And 0 < b \And a = A \And b = B --> ggt(a,b) = ggt(A,B)$
Vereinfachte Verifikationsbedingungen:
1 | $ggt(a,b) = ggt(A,B) \land true --> (ggt(a, b) = ggt(A,B))) || (ggt(b,a) = ggt(A,B))) || a = ggT(a, b)$
1 => $ggt(a,b) = ggt(A,B) \land true --> ggt(a,b) = ggt(A,B)$
2 | $0 < a \And 0 < b \And a = A \And b = B --> ggt(a,b) = ggt(A,B)$
2 => Da a = A und b = B muss $ggt(a,b) = ggt(A,B)$ sein

12.1

int factorial(int n)
/**  pre 0 ≤ n;
     post \result = n!; */
{
    int f;
    // 0 < 0 && 0 ≤ n && n == n@pre
    /** const n == n@pre */ 
    f = fact(0, n); //Fehler, hier müsste f = fact(1, n); stehen, damit die Verifikationsbedingung gilt
    // { f = n@pre! }
    return f;
    // {false | \result = n@pre! }
}

int fact(int acc, int n)
/** pre 0 ≤ n \land 0 \leq acc;
    post \result = acc * n!; */
{
    int r;

    // ((n == 0) && (acc = acc@pre * n@pre!) || ((n ≠ 0) && (0 < acc * n && 0 ≤ n && n = n@pre))
    if(n == 0) {
        // { acc = acc@pre * n@pre! }
        return acc;
        // { false | \result = acc * n!; }
    }
    /** const acc = acc@pre && n = n@pre; */ 
    r = fact(acc * n, n - 1);
    // { r = acc * n * (n-1)! && n = n@pre}
    // { r = acc@pre * n@pre! }
    return r * acc;
    // { false | \result = acc * n! }
}
            
1 | f = 0 * n! --> f = n@pre!

13.1

int *a[1];
struct {
    int p[2];
    struct {
        int x;
        int y; } q[2];
    } b;

    
|*a|b                                               	      |
   |b.p[0]  |                                    	| b.p[1]  |
   |        |b.q[0] 			| b.q[1]
   |		|b.q[0].x b.q[0].y	| b.q[1].x b.q[1].y

a[1] ist undefiniert
b.p[1] ist m.p[1]
b.q[0] ist m.q[0]
b.q[1].y ist m.q[1].y
(*b.q[1]).y ist erstmal undefiniert, weil Pointer