CISC/CMPE 223 - Assignment 4 (section 2) (Fall 2020)
Due: Thursday November 19, 2:00 PM (Kingston time)
Regulations on assignments
• The assignments are graded according to the correctness, preciseness and legibility of
the solutions. All handwritten parts, including figures, should be clear and legible. This
assignment is marked out of 20 possible marks.
• Please submit your solution in onQ before the due time.
• The assignment must be based on individual work. Copying solutions from other
students is a violation of academic integrity. See the course web site for more information
https://research.cs.queensu.ca/home/cisc223/2013w/#AS
1. (5 marks) What should the pre-condition P be in each of the following ten correctness
statements for the statement to be an instance of Hoare’s axiom scheme? All variables
are of type int.
(a) P { x = 2; } x == 1
(b) P { x = 2; } x > 2
(c) P { x = y + z; } x < y + z
(d) P { x = x + y + z; } z > x*x + 2
(e) P { x = x + y + z; } y*y > z + 5
(f) P { x = y + z } Exists(w = 0; w < 10) x + w == 50
(g) P { x = y + z; } ForAll(z = 1; z < 100) x + 2*z > w + 2
(h) P { x = y + z; } ForAll(x = 1; x < z) x + y + 2 < 100
(i) P { x = y + z; } ForAll(y = 1; y < n) Exists(z = 1; z < n) x*y <= 3*z+w
(j) P { x = y + z; } ForAll(y = 1; y < n) Exists(x = 1; x < n) x*y <= 3*z+w
2. Verify the validity of the following two correctness statements (a) and (b) by adding all
the intermediate assertions, that is, give the proof tableau showing the validity of the
correctness statement. All variables are of type int.
Also state any mathematical facts used.
(a) (2.5 marks)
ASSERT( y == 0 || z > -1 )
x = z-y;
z = x+y;
y = x-z;
ASSERT( x >= y || z == x+y )
(b) (2.5 marks)
ASSERT( true )
if (x >= y) x = y - 1; else y = y + 1;
z = y + 1;
ASSERT( x < y < z )
3. (5 marks) Write and verify a program that computes the sum of the cubes of the first n
positive integers. Below is the specification.
Declarative interface:
const int n; /* the program will compute the sum of the cubes of
the first n positive integers */
int sum; /* the sum of the cubes is stored in this variable */
Below are given the pre- and post-condition:
ASSERT( n >= 1 )
/* the program goes here */
ASSERT( sum ==
∑n
i=1 i*i*i )
The program should use a while-loop and standard arithmetic operations.
Select a loop invariant and give a complete proof tableau for the program (including all
the intermediate assertions). Also make an argument for termination.
4. (5 marks) Verify the below code using the suggested invariant. That is, give a
complete proof tableau by adding all the intermediate assertions. Also make an argument
for termination. All variables are of type int.
ASSERT(num >= 0 && den > 0)
quot = 0; rem = num;
while (rem >= den)
INVAR( num == quot * den + rem && 0 <= rem && 0 < den)
{ rem = rem - den;
quot++;
}
ASSERT( num == quot * den + rem && 0 <= rem < den)
Note: This is Exercise 3.12 in the textbook and a discussion of the code appears on page
69.

欢迎咨询51作业君