Piton A Mechanically Verified Assembly-Level Language /

• Κύριος συγγραφέας: Moore, J Strother (Συγγραφέας)
• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Dordrecht : Springer Netherlands, 1996.
• Σειρά: Automated Reasoning Series, 3
• Θέματα: Computer science.; Programming languages (Electronic computers).; Computers.; Mathematical logic.; Computer Science.; Computer Science, general.; Computing Methodologies.; Programming Languages, Compilers, Interpreters.; Mathematical Logic and Foundations.

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...

Πίνακας περιεχομένων:

• 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.