Lecture 3

This web page was written on:
30 August 2021

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