Formal Systems Development

October 10, 2020

Lecture Contents

• Lecture 1 - Introductions
• Lecture 2 - Abstract Machines, Notation
• Lecture 3 - Operations, Relations
• Lecture 4 - More Relations, Domain and Range Restriction
• Lecture 5 - Nondeterminism
• Lecture 6 - Functions
• Lecture 7 - Verification, Substitution
• Lecture 8 - Sequences
• Lecture 9 - Nondeterminism
• Lecture 10 - Arrays, Record Type, Assertions, Proof
• Lecture 11 - Structuring, SEES, USES, INCLUDES
• Lecture 12 - (Prover)
• Lecture 13 - Refinement Machines, Structure and Requirements for Refinements
• Lecture 14 - Linking Invariants, Operation Refinement
• Lecture 15 - Proof Obligations for Refinement
• Lecture 16 - Loops
• Lecture 17 - Implementation Machines, B0, Importing Machines
• Lecture 18 - Library Machines, Proving Implementations

Index

• Hoare Triples - Lecture 7, Slide 6
• Weakest Precondition - Lecture 7, Slide 8
• Substitution notation - Lecture 7, Slide 9
• Refinement Proof Obligations - Lecture 15
• Initialisation Condition - Lecture 15, Slide 13

VARIABLES
	owes, price
	
INITIALISATION
	owes = CID * {0} | price = ITEM * {0}
	
INVARIANT
	owes : CID +-> NAT & price : ITEM +-> NAT

OPERATIONS
	order(cc, ii) = PRE cc : CID & ii : ITEM THEN
		owes(cc) := owes(cc) + price(ii) END
		
	pay = PRE card(cq) > 0 THEN
		cq := tail(cq) | owes(cq(1)) = 0 END
		
	nopay = PRE card(cq) > 0 THEN cq := tail(cq) END
	
	decrease(nn) = PRE nn : NAT1 THEN 
		ANY ss WHERE ss <: ITEM & card(ss) = nn THEN
			price := {ii | ii : ss =>