Skip to content

Commit 07bdb72

Browse files
pl3onasmpl3onasm
committed
exam2-2024
1 parent 8003b49 commit 07bdb72

File tree

14 files changed

+504
-6
lines changed

14 files changed

+504
-6
lines changed

‎PF2-3/exam2-2023/problem6/sol6.dfy

+13-2
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,17 @@ ensures a == fSum(n)
2424
{
2525
k := k + 1;
2626
a := a + x;
27-
x, y := y, 2 * y + 3 * x;
27+
y := 2 * y + 3 * x;
28+
x := (y - 3 * x) / 2;
2829
}
29-
}
30+
}
31+
32+
/* Alternatively, the following loop body can be used:
33+
34+
k := k + 1;
35+
a := a + x;
36+
y, x := 2 * y + 3 * x, y;
37+
38+
It is equivalent to the loop body above,
39+
but more concise.
40+
*/

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

+106
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
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).
8+
9+
---------------
10+
11+
$\Large{\color{darkkhaki}\text{Prob 1.1}}$
12+
13+
```java
14+
// y - 2*x = 104
15+
.....
16+
// x + y = 100
17+
```
18+
19+
${\color{peru}(a)} \quad x := 2; \space y := 100;$
20+
${\color{peru}(b)} \quad y := 2*y; \space x := y - 52;$
21+
${\color{peru}(c)} \quad x := x + 2; \space y := y - 3*x;$
22+
23+
<br/>
24+
25+
---------------
26+
27+
$\Large{\color{darkkhaki}\text{Prob 1.2}}$
28+
29+
```java
30+
// x = A ∧ y = B
31+
.....
32+
// x = A - B ∧ y = A + B
33+
```
34+
35+
${\color{peru}(a)} \quad x := x - y; \space y := x + 2*y;$
36+
${\color{peru}(b)} \quad y := x + y; \space x := x - 2 * y;$
37+
${\color{peru}(c)} \quad y := x + y; \space x := y - 2 * x;$
38+
39+
<br/>
40+
41+
---------------
42+
43+
$\Large{\color{darkkhaki}\text{Prob 1.3}}$
44+
45+
```java
46+
// x = A ∧ y = B
47+
.....
48+
// x + y = A - B
49+
```
50+
51+
${\color{peru}(a)} \quad x := 0; \space y := A - B;$
52+
${\color{peru}(b)} \quad y := -y; \space x := x + y;$
53+
${\color{peru}(c)} \quad x := x - 3*y; \space y := 2*y;$
54+
55+
<br/>
56+
57+
---------------
58+
59+
$\Large{\color{darkkhaki}\text{Prob 1.4}}$
60+
61+
```java
62+
// .....
63+
x := x - 2;
64+
z := x + 1;
65+
// z ≠ 0
66+
```
67+
68+
${\color{peru}(a)} \quad x \neq -1$
69+
${\color{peru}(b)} \quad x \neq 1$
70+
${\color{peru}(c)} \quad z \neq -1$
71+
72+
<br/>
73+
74+
---------------
75+
76+
$\Large{\color{darkkhaki}\text{Prob 1.5}}$
77+
78+
```java
79+
// .....
80+
x := 2*y;
81+
z := x + y;
82+
// z > 0
83+
```
84+
85+
${\color{peru}(a)} \quad y > 0$
86+
${\color{peru}(b)} \quad x > 0$
87+
${\color{peru}(c)} \quad z > 0$
88+
89+
<br/>
90+
91+
---------------
92+
93+
$\Large{\color{darkkhaki}\text{Prob 1.6}}$
94+
95+
```java
96+
// .....
97+
x := 3*(x + 2*y - 36);
98+
y := 2*x - 10;
99+
// y > 26
100+
```
101+
102+
${\color{peru}(a)} \quad 2*x + y > 42$
103+
${\color{peru}(b)} \quad x + 2*y > 42$
104+
${\color{peru}(c)} \quad x + y \geq 42$
105+
106+
&nbsp;

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

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

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

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
/* file: prob2.dfy
2+
author: your name
3+
description: 2-3rd exam 2024, problem 2
4+
*/
5+
6+
method problem2(a:int, b:int, ghost X:int, ghost Y:int) returns (c:int, d : int)
7+
requires a == 2*X - 5*Y && b == X + 2*Y
8+
ensures c == X && d == 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+
}

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

+21
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 exam 2024, solution to problem 2
4+
*/
5+
6+
method problem2(a:int, b:int, ghost X:int, ghost Y:int) returns (c:int, d : int)
7+
requires a == 2*X - 5*Y && b == X + 2*Y
8+
ensures c == X && d == Y
9+
{
10+
// a == 2*X - 5*Y && b == X + 2*Y
11+
// (isolate Y by subracting 2*b from a)
12+
// a - 2*b == -9*Y && b == X + 2*Y
13+
// (prepare d := (2*b - a)/9)
14+
// (2*b - a) / 9 == Y && b == X + 2*Y
15+
d := (2*b - a)/9;
16+
// d == Y && b == X + 2*Y
17+
// (prepare c := b - 2*d)
18+
// d == Y && b - 2*d == X
19+
c := b - 2*d;
20+
// d == Y && c == X
21+
}

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

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
/* file: prob3.dfy
2+
author: your name
3+
description: 2-3rd exam 2024, problem 3
4+
*/
5+
6+
method problem3(a: int, n:int, ghost X: int) returns (b:int)
7+
requires a == 2*X - n || a == 3*n - 2*X + 1
8+
ensures b == X
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/exam2-2024/problem3/sol3.dfy

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

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

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
/* file: prob4.dfy
2+
author: your name
3+
description: 2-3rd exam 2024, problem 4
4+
*/
5+
6+
method problem4(a: nat, b:nat)
7+
requires a >= b
8+
{
9+
var x := a;
10+
var y := b;
11+
while x != y
12+
invariant ?? // choose a suitable invariant
13+
decreases ?? // choose a suitable variant function
14+
{
15+
y := y + 1;
16+
x := x - x % y;
17+
}
18+
assert x == y;
19+
}

‎PF2-3/exam2-2024/problem4/sol4.dfy

+21
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
/* file: sol4.dfy
2+
author: David De Potter
3+
description: 2-3rd exam 2024, solution to problem 4
4+
*/
5+
6+
method problem4(a: nat, b:nat)
7+
requires a >= b
8+
{
9+
var x := a;
10+
var y := b;
11+
while x != y
12+
invariant x >= y
13+
decreases x - y
14+
{
15+
y := y + 1;
16+
x := x - x % y;
17+
}
18+
assert x == y;
19+
}
20+
21+

0 commit comments

Comments
 (0)