| This book describes the specification and proof of a compiler for a realistically complicated assembly-level language. The book defines the state of the art in machine check proofs of software. 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? How 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 is a simple but non-trivial programming language. It provides execute-only programs, recursive subroutine call and return, stack based parameter passing, local variables, global variables and arrays, a user-visible stack for intermediate results, and seven abstract data types including integers, data addresses, program addresses and subroutine names. |
|
|
 Building Web Reputation Systems
Today’s Web is the product of over a billion hands and minds. Around the clock and around the globe, people are pumping out contributions small and large: full-length features on Vimeo, video shorts on YouTube, comments on Blogger, discussions on Yahoo! Groups, and tagged-and-titled Del.icio.us bookmarks. User-generated content... | | Getting Started with nopCommerce
You don't have to be a techie to use the power of nopCommerce to sell your products online. This guide walks you through the many features of the engine to create a complete working store in easy steps.
Overview
-
Learn to install and configure nopCommerce in order to start selling products online
... | | Precalculus
Get a good grade in your precalculus course with PRECALCULUS, Seventh Edition. Written in a clear, student-friendly style, the book also provides a graphical perspective so you can develop a visual understanding of college algebra and trigonometry. With great examples, exercises, applications, and real-life data--and a range of online study... |
Garbage and Recycling (Introducing Issues With Opposing Viewpoints)
Indulging in a wide spectrum of ideas, beliefs, and perspectives is a critical cornerstone of democracy. After all, it is often debates over differences of opinion, such as whether to legalize abortion, how to treat prisoners, or when to enact the death penalty, that shape our society and drive it forward. Such diversity of thought is... | | Data Conversion Handbook (Analog Devices)Analog-to-digital (A/D) and digital-to-analog (D/A) converters provide the link between analog data produced by sensors and transducers (links to the real world, from microphones and video cameras to radar speed guns) and the digital data of signal processing, computing and other digital data collection or data processing systems. This complete... | | Malware: Fighting Malicious CodeIgnoring the threat of malware is one of the most reckless things you can do in today's increasingly hostile computing environment. Malware is malicious code planted on your computer, and it can give the attacker a truly alarming degree of control over your system, network, and data-all without your knowledge! Written for computer pros and savvy... |
|
