Author(s)

J.C. Boarder

Abstract

Formal methods are introduced to students progressing to honours degree Computer Engineering programmes. Students use a formal system framework based on state-transition concepts. They model their own example systems abstracted from common knowledge. N-Square charts refine abstract state-transitions to an interpretable model via matrix representations. Formal system descriptions are translated to a PT Net. Drawing pin methods, supported by Marking Class Matrices, illustrate system properties. Sentential forms, syntactic consequences and semantics are demonstrated. Partial proof is also demonstrated through derivations based on transitions; initial states, as axioms, are reduced through transitions, as inference rules, to final states. Finally, students plug their formal system descri

Keywords