|
|
|---|
|
|
|
|---|
M. M. Wilding, “A
Mechanically Verified Application for a Mechanically Verified
Environment, in C. Courcoubetis, editor, Proceedings of
Computer-Aided Verification -- CAV '93, Springer-Verlag, LNCS
697, Heidelberg, pp. 268-279, DOI:10.1007/3-540-56922-7_22,
1993.
Relevance: functional correctness and resource
utilization of a Nim-playing program on the CLI Verified Stack
Abstract
We have developed a verified application proved to be both effective and efficient. The application generates moves in the puzzle-game Nim and is coded in Piton, a language with a formal semantics and a compiler verified to preserve its semantics on the underlying machine. The Piton compiler is targeted to the FM9001, a recently fabricated verified microprocessor. The Nim program correctness proof makes use of the language semantics that the compiler is proved to implement. Like the Piton compiler proof and FM9001 design proof, the Nim correctness proof is generated using Nqthm, a proof system sometimes known as the Boyer-Moore theorem prover.
The paper proves that a Piton program constructed by the author implements a winning strategy (if one exists for a given starting state) of the game of Nim. In addition, he proved a bound on the number of instructions executed on each move as well as bounds on the sizes of both the control stack and the temporary stack.
In the conclusion of the paper (page 278) the author writes
“Mechanical verification of programs in this manner is time-consuming and difficult. Nevertheless, and quite remarkably, the experience of building the Nim program suggests that development time scales linearly with program length. Once a Piton subroutine has been proved correct, a call to this subroutine can be reasoned about as easily as any basic Piton statement.
...
An FM9001 was fabricated and runs a compiled version of the Nim program. The fabricated FM9001 microprocessor, the Piton compiler, and the Nim program were never tested in a conventional manner during development or after completion. Even so, each worked the first time and we would have been surprised if any had not.”