Project 2

Following are some test cases that I’ve used for past model checking assignments. All are simple imperative programs written in a canonical block oriented style that everyone should recognize. For this project you should take each program, define a correctness invariant, and verify the correctness invariant by hand and/or using the model_check capability and small-step operational semantics defined by Chlipala. The first two should be simple as they involve no iteration. Be careful with the nested WHILE loop if you use model_check.

You may work together on these problems and we will discuss in class.

IF X <= 3 THEN IF Y <= 4 THEN Z:=X+Y
                         ELSE SKIP
          ELSE IF Y <= 4 THEN Z:=X*Y
                         ELSE Z:=1

X := 1 ; 
IF X = 3 THEN X:=1 ; Y:=4 ELSE X:=0 ENDIF ;
SKIP

Y:=0;
IF X <= 10 THEN WHILE Y <= 10 DO Y:=Y+1; X:=X+Y
           ELSE X := 10

Y := X ; 
Z := Y ;
WHILE Y <= 10 DO
  WHILE Z <= 10 DO
    X := X+Z ;
    Z := Z+1 ;
  Y := Y+1 ;
SKIP ;