Blog

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 ;
```