Review2Review Session for Second Midterm

General Notes

Hints

On each version of the exam, there will be at least one problem taken more or less verbatim from a homework assignment.
Both versions will include one or more decorated programs.
On the advanced version, there will be an informal proof.
This set of review questions is biased toward ones that can be discussed in class / using clickers, so it doesn't fully represent the range of questions that might show up on the exam.

Make sure to have a look at some prior exams to get a sense of some other sorts of questions you might see.

Definitions

On a piece of paper, write down the precise definition of what it means to say that two Imp programs are equivalent.

On a piece of paper, write down precisely what it means to say that a Hoare triple is valid.

In the Hoare chapter, we used the notation bassn b to "lift a boolean expression into an assertion." Briefly explain what this means and why it's needed.

IMP Program Equivalence

Are the two following programs equivalent?

X::= Y+1
Y::= X-1

X::= Y+1

(1) yes

(2) no (and give a counterexample)

Are the two following programs equivalent?

X::= Y-1
Y::= X+1

X::= Y-1

(1) yes

(2) no (and give a counterexample)

Are the two following programs equivalent?

IFB X ≠ 1 THEN Y ::=0 ELSE Y ::= 1 FI

IFB X > 0 THEN Y ::=0 ELSE Y ::= 1 FI

(1) yes

(2) no (and give a counterexample)

Are the two following programs equivalent?

IFB X ≠ 1 THEN Y ::= 1 ELSE Y ::= 1 FI

IFB X ≥ 0 THEN Y ::= 1 ELSE Y ::= 0 FI

(1) yes

(2) no (and give a counterexample)

Are the two following programs equivalent?

IFB X ≠ 0 THEN SKIP ELSE Y ::= 1 FI

IFB X < 0 THEN Y ::= 0 ELSE Y ::= 1 FI

(1) yes

(2) no (and give a counterexample)

Are the two following programs equivalent?

  Y ::= 0
  WHILE X > 0 DO
    Y ::= Y+X
    X ::= X-1
  END
Z ::= Y

  Y ::= 0
  WHILE X > 0 DO
    Y ::= Y+X
    Z ::= Y
    X ::= X-1
  END

(1) yes

(2) no (and give a counterexample)

Are the two following programs equivalent?

  WHILE X > 0 DO
    Y ::= Y+1
    X ::= X-1
  END

Y ::= X + Y

(1) yes

(2) no (and give a counterexample)

Are the two following programs equivalent?

  WHILE X > 0 DO
    Y ::= 0
    X ::= X+1
  END

  IF X > 0 THEN
    WHILE True DO
      Y ::= X + Y
    END
  ELSE
    SKIP
  FI

(1) yes

(2) no (and give a counterexample)

Hoare triples

Is the following Hoare triple valid ?

      {{ X = 5 ∧  Y= 6 }}
      X := Y
      {{ X = 6 ∧ Y = 6 }}

(1) yes

(2) no (and give a counterexample)

Is the following Hoare triple valid ?

      {{ X = 5 ∧  Y= 6 }}
      Y := X
      {{ X = 6 ∧ Y = 6 }}

(1) yes

(2) no (and give a counterexample)

Is the following Hoare triple valid ?

       {{ True }}
       IF Y ≤ X THEN
          X ::= Y
       ELSE
          Y ::= X
       FI
       {{ X > Y }}

(1) yes

(2) no (and give a counterexample)

Is the following Hoare triple valid ?

       {{ X = m ∧ Y = n }}
       IF Y ≤ X THEN
          X ::= Y
       ELSE
          Y ::= X
       FI
       {{ X = Y ∧  X = min(m,n) }}

(1) yes

(2) no (and give a counterexample)

Is the following Hoare triple valid ?

       {{ X = m + 1 }}
       WHILE X > 0 DO
         X ::= X+1
       END
       {{ False }}

(1) yes

(2) no (and give a counterexample)

Decorated programs

Fill in valid decorations for the following program:

  {{ X = m ∧ Y = n }}
  IF Y ≤ X THEN
     {{                          }} ⇾
     {{                          }}
    X ::= Y
     {{                          }}
  ELSE
     {{                          }} ⇾
     {{                          }}
     Y ::= X
     {{                          }}
  FI
  {{ X = Y ∧  Y = min(m,n) }}

Fill in valid decorations for the following program:

  {{ TRUE }}
  X ::= 0
  {{                  }}
  Z ::= 0
  {{                  }}
  WHILE X ≠ n DO
    {{                }} ⇾
    {{                }}
    Y ::= 0
    {{                }}
    WHILE Y ≠ m DO
      {{                     }} ⇾
      {{                     }}
      Z ::= Z + 1
      {{                     }}
      Y ::= Y + 1
      {{                     }}
    END
    {{                }} ⇾
    {{                }}
    X ::= X + 1
    {{                }}
  END
  {{                  }} ⇾
  {{ Z = n × m }}