CSSE3100/7100 Reasoning about Programs
Week 1 Exercises
Exercise 1.1.
(a) Below is the Dafny type signature of a method to compute s to be the sum of x and y and
m to be the maximum of x and y:
method MaxSum(x: int, y: int) returns (s: int, m: int)
Write the postcondition of this method.
(b) Consider a Dafny method that attempts to reconstruct possible arguments x and y from the return values of MaxSum in Exercise 1.1. In other words, consider a method with the
following type signature and the postcondition from Exercise 1.1.
method ReconstructFromMaxSum(s: int, m: int) returns (x: int, y: int)
ensures your answerfrom Exercise 1.1.
This method cannot be implemented. Why not? Write an appropriate precondition for the method that allows you to implement the method.
Exercise 1.2.
For each of the following explain why the verification fails in the Dafny verifier, and what you need to change to make them verify.
(a) function F(): int {
29
}
method M() returns (r: int) {
r := 29;
}
method Caller() returns (a: int, b: int)
ensures a == 29
ensures b == 29 // this postcondition is not satisfied
{
a := F();
b := M();
}
(b) method Index(n: int) returns (i: int)
requires n >= 1
ensures 0 <= i < n
{
i := n/2;
}
method IndexCaller() returns (x: int, y: int)
ensures x == y // this postcondition is not satisfied
{
x := Index(50);
y := Index(50);
}
For the remaining exercises,justify your proof steps using the predicate logic below.
Exercise 1.3.
Prove the following using only De Morgan's Law: !(X || Y) = !X && !Y and laws of ! and &&.
a) X || true == true
b) X || X == X
c) X || Y == Y || X
Exercise 1.4.
Prove the following variations of De Morgan's Law.
a) X || Y == !(!X && !Y)
b) X && Y == !(!X || !Y)
Exercise 1.5.
Prove the following.
a) X && (X ==> Y) == X && Y
b) X ==> Y == !Y ==> !X
c) X && Y ==> Z == X ==> !Y || Z
d) X || Y ==> Z == (X ==> Z) && (Y ==> Z)
e) X || (!X ==> Y) == X || Y
f) X ==> Y && Z == (X ==> Y) && (X ==> Z)
Exercise 1.6.
Prove that each of the following hold by simplifying the antecedent (i.e., LHS) of the implication. (For (b), you need to use some simple properties of arithmetic).
a) (P && Q ==> R) && !R && P ==> !Q
b) (x < 5 ==> y == 10) && y < 7 && (y < 1000 ==> x <= 5) ==> x == 5
|
Selection of predicate logic laws (from Programming from Specifications, Appendix A)
Conjunction and disjunction
A && A == A = A || A (A.1)
A && B == B && A (A.2)
A || B == B || A (A.3)
A && (B && C) == (A && B) && C (A.4)
A || (B || C) == (A || B) || C (A.5)
A && (A || B) == A == A || (A && B) (A.6)
A && (B || C) == (A && B) || (A && C) (A.7)
A || (B && C) == (A || B) && (A || C) (A.8)
A && true == A (A.9)
A || true == true (A.10)
A && false == false (A.11)
A || false == A (A.12)
Negation
!true == false (A.13)
!false == true (A.14)
A && !A == false (A.15)
A || !A == true (A.16)
!!A == A (A.17)
DeMorgan's laws
!(A && B) == !A || !B (A.18)
!(A || B) == !A && !B (A.19)
Implication
A ==> B == !A || B (A.22)
|