Lecture 3

This web page was written on:
7 April 2017

The video was produced on:
7 April 2017

Copy the following tiny text, either by clicking on the Copy button below it, or by your usual method of copying text.

EXTENDS Integers
VARIABLES i, pc   

Init == (pc = "start") /\ (i = 0)

Pick == /\ pc = "start"  
        /\ i' \in 0..1000
        /\ pc' = "middle"

Add1 == /\ pc = "middle" 
        /\ i' = i + 1
        /\ pc' = "done"  
           
Next == Pick \/ Add1

Then paste the text into the module editor as the body of specification SimpleProgram .

The Next Video

Die Hard