Program Models: Meaning and Proof

Resumé

When does one understand a program P? One reasonable answer is: when one has a conceptually clear model M such that any relevant question about P can be reformulated as a logically equivalent question about M. This paper argues for diagram models of parallel programs as a simple generalization of the familiar flowchart, graph and equation-set models of sequential programs. Diagram models of Petri nets were introduced by Hinderer.