# 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 }}