Lecture 3

This web page was written on:
  20 July 2019

The video was produced on:
   7 April 2017

Click here for downloading and installation instructions

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