Computer Science · Formal Methods & Verification
A topic within Formal Methods & Verification, itself one of 9 topics in that field and part of Computer Science.
2 works
J.M. Spivey
Defines Z's set-theoretic and schema notation precisely enough to serve as its own standard, giving specifiers a mathematical language for describing what a system must do before anyone writes code.
Leslie Lamport
Introduces TLA+ and argues that writing a precise specification of a concurrent system, before coding it, is what actually catches its bugs.
Assumes predicate logic and set theory, and a willingness to write the specification before the code
link checked 17 Sept 2026