Piton: A Mechanically Verified Assembly-Level LanguageКНИГИ » ПРОГРАММИНГ
Автор: J Strother Moore Название: Piton: A Mechanically Verified Assembly-Level Language Издательство: Springer Год: 1996 Серия: Automated Reasoning Series ISBN: 0792339207 Язык: English Формат: pdf Размер: 11,4 mb Страниц: 320
Piton is a simple assembly-level programming language for a microprocessor called the FM9001 described at the machine code level. The correctness of the implementation has been proved by a mechanical theorem prover.
This book is about the exact meaning of the previous paragraph. What is Piton, exactly? What is the FM9001? How is Piton implemented on the FM9001? In what sense is the implementation correct? How is its correctness expressed mathematically? Ho|w is it proved? These questions are answered here. Also discussed is the evolutionary character of software, the Piton implementation in particular, and how proof plays a continuing role in its design and improvement.
Навигация
Вход на сайт
Реклама
Piton: A Mechanically Verified Assembly-Level Language 
