Piton_ A Mechanically Verified Assembly-Level Language [Moore 2013-04-24].pdf

(11704 KB) Pobierz
Piton
Automated Reasoning Series
VOLUME 3
Managing Editor
William Pase,
Odyssey Research Associates, Ottawa, Canada
Editorial Board
Robert S. Boyer,
University of Texas at Austin
Deepak Kapur,
State University of New York at Albany
Hans Jiirgen Ohlbach,
Max-Planck-Institut fUr Informatik
Lawrence Paulson,
Cambridge University
Mark Stickel,
SRI International
Richard Waldinger,
SRI International
Larry Wos,
Argonne National Laboratory
Piton
A Mechanically Verified
Assembly-Level Language
by
J STROTHER MOORE
Computational Logic, Inc.,
Austin, Texas, U.SA.
WKAP ARCHIEF
KLUWER ACADEMIC PUBLISHERS
A C.I.P. Catalogue record for this book is available from the Library of Congress.
ISBN 0-7923-3920-7
Published by Kluwer Academic Publishers,
P.O. Box 17, 3300 AA Dordrecht, The Netherlands.
Kluwer Academic Publishers incorporates
the publishing prograimnes of
D. Reidel, Martinus Nijhoff, Dr W. Junk and MTP Press.
Sold and distributed in the U.S.A. and Canada
by Kluwer Academic Publishers,
101 Philip Drive, NorweU, MA 02061, U.S.A.
In all other countries, sold and distributed
by Kluwer Academic Publishers Group,
P.O. Box 322, 3300 AH Dordrecht, The Netherlands.
Printed on acid-free paper
All Rights Reserved
© 1996 Kluwer Academic Publishers
No part of the material protected by this copyright notice may be reproduced or
utilized in any form or by any means, electronic or mechanical,
including photocopying, recording or by any information storage and
retrieval system, without written permission frorh the copyright owner.
Printed in the Netherlands
Contents
Preface
1. Introduction and History
1.1.
1.2.
1.3.
1.4.
1.5.
1.6.
1.7.
2.1.
2.2.
2.3.
2.4.
2.5.
3.1.
3.2.
3.3.
3.4.
3.5.
3.6.
3.7.
3.8.
3.9.
4.1.
4.2.
4.3.
4.4.
4.5.
4.6.
4.7.
4.8.
What This Book is About
Piton as a Software Project
About This Book
Mechanized Mathematics and the Social Process
The History of the Piton Project
Related Work
Outline of the Presentation
Syntax, Primitive Data Types and Conventions
Primitive Function Symbols
Let Notation
Recursive Definitions
User-Defined Data Types
An Example Piton Program
Piton States
Type Checking
Data Types
The Data Segment
The Program Segment
Instructions
The Piton Interpreter
Erroneous States
An Informal Explanation
A Formal Explanation
A Piton Program
An Initial State
The Formal Specification
Using the Formal Specification
The Proof of the Correctness of Big-Add
Summary
vii
1
1
3
4
6
8
13
15
2. The Nqtlim Logic
17
18
19
22
22
23
3. An Informal Sketch of Piton
25
26
27
28
29
31
33
34
39
40
4. Big Number Addition
43
43
44
47
47
52
59
65
70

Plik z chomika:

Inne pliki z tego folderu:

Inne foldery tego chomika:

Zgłoś jeśli naruszono regulamin