Piton A Mechanically Verified Assembly-Level Language /

• Main Author: Moore, J Strother. (Author)
• Corporate Author: SpringerLink (Online service)
• Format: Electronic
• Language: English
• Published: Dordrecht : Springer Netherlands, 1996.
• Series: Automated Reasoning Series, 3
• Subjects: Computer science.; Programming languages (Electronic computers).; Computers.; Mathematical logic.; Computer Science.; Computer Science, general.; Computing Methodologies.; Programming Languages, Compilers, Interpreters.; Mathematical Logic and Foundations.
• Online Access: View fulltext via EzAccess

Mountaineers use pitons to protect themselves from falls. The lead climber wears a harness to which a rope is tied. As the climber ascends, the rope is paid out by a partner on the ground. As described thus far, the climber receives no protection from the rope or the partner. However, the climber ge...

Table of Contents:

• and History
• The Nqthm Logic
• An Informal Sketch of Piton
• Big Number Addition
• A Sketch of FM9001
• The Correctness of Piton on FM9001
• The Implementation of Piton on FM9001
• Proof of the Correctness Theorem.