Skip to content

Commit 4a03655

Browse files
pl3onasmpl3onasm
committed
PF2-3 resit-2024
1 parent 6acc74a commit 4a03655

File tree

16 files changed

+537
-6
lines changed

16 files changed

+537
-6
lines changed

‎PF2-3/exam2-2024/problem1/prob1.md

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,7 @@ $\huge\color{cadetblue}{\text{Problem 1}}$
22

33
<br/>
44

5-
For each of the following annotations determine which choice fits on the empty line (.....). The
6-
variables x, y, and z are of type int. Note that A and B (capital letters!) are specification
7-
constants (so not program variables).
5+
For each of the following annotations determine which choice fits on the empty line (.....). The variables x, y, and z are of type int. Note that A and B (capital letters!) are specification constants (so not program variables).
86

97
---------------
108

‎PF2-3/exam2-2024/problem5/sol5.dfy

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ ensures x == f(n)
1919
var k: nat := n;
2020
var z: int := 0;
2121

22-
while k >= 2
22+
while k > 0
2323
invariant f(n) == x + z + y * f(k)
2424
decreases k
2525
{
@@ -33,6 +33,6 @@ ensures x == f(n)
3333
k := k / 2;
3434
}
3535
assert x + y > -z;
36-
x := x + y + z;
36+
x := x + y + z; // active finalization
3737
}
3838

‎PF2-3/resit2-2023/problem2/sol2.dfy

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55

66
method problem2(m:int, n:int, X:int, Y:int) returns (x:int, y:int)
77
requires 3*m + 2*n == 2*X + Y && 2*m == X + Y
8-
ensures x==X && y == Y
8+
ensures x == X && y == Y
99
{
1010
// 3*m + 2*n - 2*m == 2*X + Y - X - Y
1111
// m + 2*n == X

‎PF2-3/resit2-2024/problem1/prob1.md

Lines changed: 106 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,106 @@
1+
$\huge\color{cadetblue}{\text{Problem 1}}$
2+
3+
<br/>
4+
5+
For each of the following annotations determine which choice fits on the empty line (.....). The variables x, y, and z are of type int. Note that A and B (capital letters!) are specification constants (so not program variables).
6+
7+
---------------
8+
9+
$\Large{\color{darkkhaki}\text{Prob 1.1}}$
10+
11+
```java
12+
// x = A
13+
.....
14+
// x = 3 * A + 18
15+
```
16+
17+
${\color{peru} (a) } \quad x := 3 * x + 18; $
18+
${\color{peru}(b)} \quad x := x/3 - 18; $
19+
${\color{peru}(c)} \quad x := (x - 18)/3; $
20+
21+
<br/>
22+
23+
---------------
24+
25+
$\Large{\color{darkkhaki}\text{Prob 1.2}}$
26+
27+
```java
28+
// 4 * x + 2 * y + 2 * z = 2 * A
29+
.....
30+
// x = A
31+
```
32+
33+
${\color{peru}(a)} \quad x := x/2 + y; \space x := y/2 + z;$
34+
${\color{peru}(b)} \quad x := 2 * x - y; \space x := x + 2 * y + z;$
35+
${\color{peru}(c)} \quad x := 2 * x + z; \space x := x - y;$
36+
37+
<br/>
38+
39+
---------------
40+
41+
$\Large{\color{darkkhaki}\text{Prob 1.3}}$
42+
43+
```java
44+
// 3 ≤ x + y * y < 12
45+
.....
46+
// 5 ≤ y < 14
47+
```
48+
49+
${\color{peru}(a)} \quad y := x + y * y + 2;$
50+
${\color{peru}(b)} \quad y := x + y * y - 2;$
51+
${\color{peru}(c)} \quad y := y * y; \space x := 2;$
52+
53+
<br/>
54+
55+
---------------
56+
57+
$\Large{\color{darkkhaki}\text{Prob 1.4}}$
58+
59+
```java
60+
// x = A ∧ y = B
61+
x := 2 * x - y;
62+
y := y + x;
63+
x := x - y;
64+
// .....
65+
```
66+
67+
${\color{peru}(a)} \quad x = -B \land y = 2 * A$
68+
${\color{peru}(b)} \quad x = B \land y = 2 * A$
69+
${\color{peru}(c)} \quad x = 2 * A \land y = -B$
70+
71+
<br/>
72+
73+
---------------
74+
75+
$\Large{\color{darkkhaki}\text{Prob 1.5}}$
76+
77+
```java
78+
// 4 * x + 2 * y + 2 * z < 12
79+
y := y + z;
80+
x := 2 * x + y;
81+
// .....
82+
```
83+
84+
${\color{peru}(a)} \quad 8 * x < 6$
85+
${\color{peru}(b)} \quad x \leq 5$
86+
${\color{peru}(c)} \quad x < 5$
87+
88+
<br/>
89+
90+
---------------
91+
92+
$\Large{\color{darkkhaki}\text{Prob 1.6}}$
93+
94+
```java
95+
// x = A ∧ y = B
96+
x := 2 * x + 2 * y;
97+
y := x - 2 * y;
98+
x := (x - y)/2;
99+
// .....
100+
```
101+
102+
${\color{peru}(c)} \quad x = A \land y = 2 * B$
103+
${\color{peru}(c)} \quad x = B \land y = A$
104+
${\color{peru}(c)} \quad x = B \land y = 2 * A$
105+
106+
&nbsp;

‎PF2-3/resit2-2024/problem1/sol1.md

Lines changed: 144 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,144 @@
1+
$\huge\color{cadetblue}{\text{Problem 1}}$
2+
3+
---------------
4+
5+
$\Large{\color{darkkhaki}\text{Prob 1.1: }}\space{\Large\color{olive}\text{a}}$
6+
7+
```java
8+
// x = A
9+
.....
10+
// x = 3 * A + 18
11+
```
12+
13+
$\quad \lbrace \space x = A \space \rbrace$
14+
$\qquad \color{darkseagreen} (\space \text{prepare } x := 3 * x + 18 \space)$
15+
$\quad \lbrace \space 3 * x = 3 * A \space \rbrace$
16+
$\quad \lbrace \space 3 * x + 18 = 3 * A + 18 \space\rbrace$
17+
$\space \color{cornflowerblue} x := 3 * x + 18;$
18+
$\quad \lbrace \space x = 3 * A + 18 \space \rbrace$
19+
20+
<br/>
21+
22+
---------------
23+
24+
$\Large{\color{darkkhaki}\text{Prob 1.2: }}\space{\Large\color{olive}\text{b}}$
25+
26+
```java
27+
// 4 * x + 2 * y + 2 * z = 2 * A
28+
.....
29+
// x = A
30+
```
31+
32+
$\quad \lbrace \space 4 * x + 2 * y + 2 * z = 2 * A \space \rbrace$
33+
$\qquad \color{darkseagreen} (\space \text{prepare } x := 2 * x - y \space)$
34+
$\quad \lbrace\space 2 * (2 * x - y ) + 4 * y + 2 * z = 2 * A \space \rbrace$
35+
$\space \color{cornflowerblue} x := 2 * x - y;$
36+
$\quad \lbrace\space 2 * x + 4 * y + 2 * z = 2 * A \space\rbrace$
37+
$\qquad \color{darkseagreen} (\space \text{prepare } x := x + 2 * y + z \space)$
38+
$\quad \lbrace\space x + 2 * y + z = A \space\rbrace$
39+
$\space \color{cornflowerblue} x := x + 2 * y + z;$
40+
$\quad \lbrace \space x = A \space \rbrace$
41+
42+
<br/>
43+
44+
---------------
45+
46+
$\Large{\color{darkkhaki}\text{Prob 1.3: }}\space{\Large\color{olive}\text{a}}$
47+
48+
```java
49+
// 3 ≤ x + y * y < 12
50+
.....
51+
// 5 ≤ y < 14
52+
```
53+
54+
$\quad \lbrace \space 3 \leq x + y * y < 12 \space \rbrace$
55+
$\qquad \color{darkseagreen} (\space \text{prepare } y := x + y * y + 2 \space)$
56+
$\quad \lbrace \space 5 \leq x + y * y + 2 < 14 \space \rbrace$
57+
$\space \color{cornflowerblue} y := x + y * y + 2;$
58+
$\quad \lbrace \space 5 \leq y < 14 \space \rbrace$
59+
60+
<br/>
61+
62+
---------------
63+
64+
$\Large{\color{darkkhaki}\text{Prob 1.4: }}\space{\Large\color{olive}\text{a}}$
65+
66+
```java
67+
// x = A ∧ y = B
68+
x := 2 * x - y;
69+
y := y + x;
70+
x := x - y;
71+
// .....
72+
```
73+
74+
$\quad \lbrace \space x = A \space \land \space y = B \space \rbrace$
75+
$\qquad \color{darkseagreen} (\space \text{prepare } x := 2 * x - y \space)$
76+
$\quad \lbrace \space 2 * x = 2 * A \space \land \space y = B \space \rbrace$
77+
$\quad \lbrace \space 2 * x - y = 2 * A - B \space \land \space y = B \space \rbrace$
78+
$\space \color{cornflowerblue} x := 2 * x - y;$
79+
$\quad \lbrace \space x = 2 * A - B \space \land \space y = B \space \rbrace$
80+
$\qquad \color{darkseagreen} (\space \text{prepare }y := y + x \space)$
81+
$\quad \lbrace \space x = 2 * A - B \space \land \space y + x = 2 * A \space \rbrace$
82+
$\space \color{cornflowerblue} y := y + x;$
83+
$\quad \lbrace \space x = 2 * A - B \space \land \space y = 2 * A \space \rbrace$
84+
$\qquad \color{darkseagreen} (\space \text{prepare }x := x - y \space)$
85+
$\quad \lbrace \space x - y = - B \space \land \space y = 2 * A \space \rbrace$
86+
$\space \color{cornflowerblue} x := x - y;$
87+
$\quad \lbrace \space x = - B \space \land \space y = 2 * A \space \rbrace$
88+
89+
<br/>
90+
91+
---------------
92+
93+
$\Large{\color{darkkhaki}\text{Prob 1.5: }}\space{\Large\color{olive}\text{b}}$
94+
95+
```java
96+
// 4 * x + 2 * y + 2 * z < 12
97+
y := y + z;
98+
x := 2 * x + y;
99+
// .....
100+
```
101+
102+
$\quad \lbrace \space 4 * x + 2 * y + 2 * z < 12 \space \rbrace$
103+
$\qquad \color{darkseagreen} (\space \text{prepare } y := y + z \space)$
104+
$\quad \lbrace \space 4 * x + 2 * (y + z) < 12 \space \rbrace$
105+
$\space \color{cornflowerblue} y := y + z;$
106+
$\quad \lbrace \space 4 * x + 2 * y < 12 \space \rbrace$
107+
$\qquad \color{darkseagreen} (\space \text{prepare } x := 2 * x + y; \space)$
108+
$\quad \lbrace \space 2 * x + * y < 6 \space \rbrace$
109+
$\space \color{cornflowerblue} x := 2 * x + y;$
110+
$\quad \lbrace \space x < 6 \space \rbrace$
111+
$\qquad \color{darkseagreen} (\space \text{arithmetic} \space)$
112+
$\quad \lbrace \space x \leq 5 \space \rbrace$
113+
<br/>
114+
115+
---------------
116+
117+
$\Large{\color{darkkhaki}\text{Prob 1.6: }}\space{\Large\color{olive}\text{c}}$
118+
119+
```java
120+
// x = A ∧ y = B
121+
x := 2 * x + 2 * y;
122+
y := x - 2 * y;
123+
x := (x - y)/2;
124+
// .....
125+
```
126+
127+
$\quad \lbrace \space \space x = A \space \land \space y = B \space \rbrace$
128+
$\qquad \color{darkseagreen} (\space \text{prepare } x := 2 * x + 2 * y \space)$
129+
$\quad \lbrace \space \space 2 * x = 2 * A \space \land \space y = B \space \rbrace$
130+
$\quad \lbrace \space \space 2 * x + 2 * y = 2 * A + 2 * B \space \land \space y = B \space \rbrace$
131+
$\space \color{cornflowerblue} x := 2 * x + 2 * y;$
132+
$\quad \lbrace \space \space x = 2 * A + 2 * B \space \land \space y = B \space \rbrace$
133+
$\qquad \color{darkseagreen} (\space \text{prepare } y := x - 2 * y \space)$
134+
$\quad \lbrace \space \space x = 2 * A + 2 * B \space \land \space - 2 * y = - 2 * B \space \rbrace$
135+
$\quad \lbrace \space \space x = 2 * A + 2 * B \space \land \space x - 2 * y = 2 * A \space \rbrace$
136+
$\space \color{cornflowerblue} y := x - 2 * y;$
137+
$\quad \lbrace \space \space x = 2 * A + 2 * B \space \land \space y = 2 * A \space \rbrace$
138+
$\qquad \color{darkseagreen} (\space \text{prepare } x := (x - y)/2 \space)$
139+
$\quad \lbrace \space \space x - y = 2 * B \space \land \space y = 2 * A \space \rbrace$
140+
$\quad \lbrace \space \space (x - y) / 2 = B \space \land \space y = 2 * A \space \rbrace$
141+
$\space \color{cornflowerblue} x := (x - y)/2;$
142+
$\quad \lbrace \space \space x = B \space \land \space y = 2 * A \space \rbrace$
143+
144+
<br/>

‎PF2-3/resit2-2024/problem2/prob2.dfy

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
/* file: prob2.dfy
2+
author: your name
3+
description: 2-3rd resit 2024, problem 2
4+
*/
5+
6+
method problem2(m:int, n:int, ghost X:int, ghost Y:int) returns (x:int, y:int)
7+
requires m + n == 3*X + 2*Y && 2*m + 3*n == 5*X + 7*Y
8+
ensures x==X && y == Y
9+
{
10+
// X and Y are specification constants and are not allowed
11+
// to appear in the body of this method.
12+
//
13+
// implement yourself
14+
15+
}
16+

‎PF2-3/resit2-2024/problem2/sol2.dfy

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
/* file: sol2.dfy
2+
author: David De Potter
3+
description: 2-3rd resit 2024, solution to problem 2
4+
*/
5+
6+
method problem2(m:int, n:int, ghost X:int, ghost Y:int) returns (x:int, y:int)
7+
requires m + n == 3*X + 2*Y && 2*m + 3*n == 5*X + 7*Y
8+
ensures x == X && y == Y
9+
{
10+
// m + n == 3*X + 2*Y && 2*m + 3*n == 5*X + 7*Y
11+
// (isolate X in the first equality)
12+
// 3*m + n == 11*X && 2*m + 3*n == 5*X + 7*Y
13+
x := (3*m + n) / 11;
14+
// x == X && 2*m + 3*n == 5*X + 7*Y
15+
// (substitute x for X in the second equality)
16+
// x == X && 2*m + 3*n == 5*x + 7*Y
17+
// (isolate Y in the second equality)
18+
// x == X && (2*m + 3*n - 5*x)/7 == Y
19+
y := (2*m + 3*n - 5*x) / 7;
20+
// x == X && y == Y
21+
}

‎PF2-3/resit2-2024/problem3/prob3.dfy

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
/* file: prob3.dfy
2+
author: your name
3+
description: 2-3rd resit 2024, problem 3
4+
*/
5+
6+
method problem3(n:int, ghost X: int) returns (r:int)
7+
requires n == X
8+
ensures r >= 0 && (r + X == 0 || 3*r <= X + 1 < 3*(r + 1))
9+
{
10+
// X is a specification constant and is not allowed
11+
// to appear in the body of this method.
12+
//
13+
// implement yourself.
14+
15+
}

‎PF2-3/resit2-2024/problem3/sol3.dfy

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
/* file: sol3.dfy
2+
author: David De Potter
3+
description: 2-3rd resit 2024, solution to problem 3
4+
*/
5+
6+
method problem3(n:int, ghost X: int) returns (r:int)
7+
requires n == X
8+
ensures r >= 0 && (r + X == 0 || 3*r <= X + 1 < 3*(r + 1))
9+
{
10+
if n < 0 {
11+
r := -n;
12+
assert r >= 0;
13+
assert r + X == 0;
14+
} else {
15+
// 3*r <= X + 1 < 3*(r + 1)
16+
// r <= (X + 1)/3 < r + 1
17+
// r == (X + 1)/3
18+
r := (n + 1) / 3;
19+
assert r >= 0;
20+
assert 3*r <= X + 1 < 3*(r + 1);
21+
}
22+
// collect branches
23+
assert r >= 0 && (r + X == 0 || 3*r <= X + 1 < 3*(r + 1));
24+
}

‎PF2-3/resit2-2024/problem4/prob4.dfy

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
/* file: prob4.dfy
2+
author: your name
3+
description: 2-3rd resit 2024, problem 4
4+
*/
5+
6+
method problem4(a:nat, b:nat) returns (x:nat)
7+
requires a > 0 && b > 0
8+
{
9+
var y:nat;
10+
x := a;
11+
y := b;
12+
while x != y
13+
// find a suitable invariant and decreases clause such
14+
// that Dafny is able to prove termination
15+
invariant ??
16+
decreases ??
17+
{
18+
if x > y {
19+
x := x - y;
20+
} else {
21+
y := y - x;
22+
}
23+
}
24+
}

0 commit comments

Comments
 (0)