CSCI 2600 Homework 1 Reasoning About Code solution

Description

Reasoning About Code

Problems

Directions:

• Assume that all numerical values are integers, and that integer overflow will never occur.
• In your answers, you may use any standard symbols for “and” and “or” (& and |, ∧ and ∨, etc.).
• If no precondition is required for a code sequence, simply write {true} to denote the trivial precondition.

Problem 1 (6pts, 1pt each): Condition Strength

1. Indicate the weakest condition in each set. Note: write “None” if the conditions are unrelated by implication. Assume x is an int.

1. { x is divisible by 10 }

{ x is divisible by 20 }

2. { 0 ≤ x ≤ 5 }

{ 0 ≤ x ≤ 3 }

{ x = 1 }

3. { x > 0 && y > 0 }

{ x > 0 || z > 0 }

4. { x = 5 && y % 2 = 0 }

{ x = 5 && y % 4 = 2 }

5. { x is prime }

{ x is odd }

6. Assume the following class hierarchy: C is a subclass of B and B is a subclass of A.

{ x is an object of type A }

{ x is an object of type C }

{ x is an object of type B }

Problem 2 (8pts, 2pts each): Hoare Triples

State whether each Hoare triple is valid. If it is invalid, explain why and show how you would modify the precondition or postcondition to make it valid.

1. { x < -1 }
   y = 2 * x;
   { y < -1 }

2. { x ≥ y }  
   z = x – y;
   { z ≥ 0 }

3. { true }

if (x % 2 == 0)

y = x;

else

y = x + 1;

{ y is even }

4. P, S, T, and U are logical conditions (logical formulae).

S => T (S implies T, i.e. S is stronger than T)

T=> U

{Q} code {T} is a valid Hoare triple. Which of the following is true?

{Q} code {S}

{Q} code {U}

If you cannot assert true, then give a counterexample. That is, give concrete values of Q, S, T, U and code that lead to an invalid triple.

Problem 3 (10pts, 2pts each): Forward reasoning with assignment statements

Find the strongest postcondition of each code sequence by inserting the appropriate condition in each blank. The first condition in part (a) is supplied as an example. Please simplify your answers as much as possible.

1. { x > 0 }
   x = 10;

   { x = 10 }

   y = 2 * x;

   {_______________________________}

   z = y + 4;

   {_______________________________}

   x = z / 2;

   {_______________________________}

   y = 0;

   {_______________________________}

2. { x > 0 }
   y = x;

   {_______________________________}

   y = y + 2;

   {_______________________________}

3. { |x| > 10 }
   x = -x;

   {_______________________________}

   x = x / 2;

   {_______________________________}

   x = x + 1;

   {_______________________________}

4. { y is odd }
   z = y * y;

   {_______________________________}

   w = z mod 4; // x mod y divides x by y and returns the integer remainder.

   {_______________________________}

5. { y > 2x }
   y = y + 2;

   {_______________________________}

   x = x + 1;
         {_______________________________}

Problem 4 (8pts, 2pts each): Backward reasoning with assignment statements

Find the weakest precondition of each code sequence by inserting the appropriate condition in each blank. Please simplify your answers as much as possible

1.      {___________________________}
   x = x + 5;
        {___________________________}
   y = 2 * x;
        { y > 10 }

2.      {___________________________}
   x = y - 10;
        {___________________________}
   z = x + y;
        { z ≤ 0 }

3.      {___________________________}
   y = 2*w + 10;
        {___________________________}
   x = 2*x;
        { x > y }

4.      {___________________________}

      t = 2 * s;
           {___________________________}
      r = w + 4;
           {___________________________}
      s = 2*s + w;
           { r > s && s > t}

Problem 5 (2pts): Backward reasoning with if/else statements

Find the weakest precondition for the conditional statement below using backward reasoning, inserting the appropriate condition in each blank. Please simplify your answers as much as possible.

{___________________________}
if (x ≥ 0)
    {___________________________}
    z = x;
    {___________________________}
else
    {___________________________}
    z = x + 1;
    {___________________________}
{z ≠ 0 }

Problem 6 (4pts, 2pts each): Verifying Correctness

For each block of code, fill in the intermediate conditions, then use them to state whether the precondition is sufficient to guarantee the postcondition. If the precondition is insufficient, explain why and indicate where the conditions don’t match up.

Hint: for assignment statements, use backward reasoning to find the weakest precondition that guarantees the postcondition, then see if the given precondition is weaker than the weakest precondition. For if/else statements, you may find a combination of forward and backward reasoning most useful. Follow the rules given in class for what condition to insert at each point. We strongly encourage that you verify your answers with Dafny. (Submission of Dafny code is not required for this problem.)

1. { x > 0 }
   z = x - 1;
   {___________________________}
   w = 2 * z;
   {___________________________}
   w = w + 1;
   {w > 1}

2. { y ≥ w }
   x = w + 2;
   {___________________________}
   y = y + 2;
   {___________________________}
   z = y;
   { z ≥ x }

Problem 7 (10pts, 5pts each): Loops

1. For the loop below, state a suitable loop invariant and decrementing function. Verify your answer with Dafny. Show your Dafny code.

   { x ≥ 0 && y ≥ 0 }
   int s = x;
   int i = y;
   while (i != 0) {
     s = s - 1;
     i = i - 1; 
   }
   {s = x - y}

2. Write a loop that computes the minimal value in a non-empty array of integers.

   { arr != null ∧ arr.Length > 0 } /* Precondition using Dafny syntax */ 
   i = 0;
   z = arr[i];
   while ( ... ) {
   
     ...
   
   }

   What is your loop invariant? What is your decrementing function? Verify your answer with Dafny. Show your Dafny code.

Collaboration (1pt)

Please answer the following questions in a file named collaboration.txt in your hw1/answers/ directory.

The standard academic integrity policy applies to this homework.

State whether or not you collaborated with other students. If you did collaborate with other students, state their names and a brief description of how you collaborated.

Reflection (1pt)

Please answer the following questions in a file named reflection.txt in your hw1/answers/ directory. Answer briefly, but in enough detail to help you improve your own practice via introspection and to enable me to improve Principles of Software in the future.

1. In retrospect, what could you have done better to reduce the time you spent solving this homework?
2. What could I (the instructor) have done better to improve your learning experience in this homework?
3. What do you know now that you wish you had known before beginning the homework?

Errata

None yet.