Muutke küpsiste eelistusi

Program Proofs [Pehme köide]

5.00/5 (2 hinnangut Goodreads-ist)
,
  • Formaat: Paperback / softback, 496 pages, kõrgus x laius: 229x178 mm, 20 line drawings, 30 figures
  • Ilmumisaeg: 07-Mar-2023
  • Kirjastus: MIT Press
  • ISBN-10: 026254623X
  • ISBN-13: 9780262546232
Teised raamatud teemal:
Program ProofsSuurem pilt
  • Formaat: Paperback / softback, 496 pages, kõrgus x laius: 229x178 mm, 20 line drawings, 30 figures
  • Ilmumisaeg: 07-Mar-2023
  • Kirjastus: MIT Press
  • ISBN-10: 026254623X
  • ISBN-13: 9780262546232
Teised raamatud teemal:
Püsilink: https://www.kriso.ee/db/9780262546232.html
Märksõnad:
"The book shows what it means to write specifications for programs, what it means for programs to satisfy those specifications, and how to write proofs that connect specifications and programs"--

This comprehensive and highly readable textbook teaches how to formally reason about computer programs using an incremental approach and the verification-aware programming language Dafny.

Program Proofs shows students what it means to write specifications for programs, what it means for programs to satisfy those specifications, and how to write proofs that connect specifications and programs. Writing with clarity and humor, K. Rustan M. Leino first provides an overview of the basic theory behind reasoning about programs. He then gradually builds up to complex concepts and applications, until students are facing real programs using objects, data structures, and non-trivial recursion. To emphasize the practical nature of program proofs, all material and examples use the verification-aware programming language Dafny, but no previous knowledge of Dafny is assumed.

  • Written in a highly readable and student-friendly style
  • Builds up to complex concepts in an incremental manner 
  • Comprehensively covers how to write proofs and how to specify and verify both functional programs and imperative programs
  • Uses real program text from a real programming language, not psuedo code
  • Features engaging illustrations and hands-on learning exercises 
Preface ix
Notes for Teachers xv
0 Introduction
1(8)
0.0 Prerequisites
2(2)
0.1 Outline of Topics
4(1)
0.2 Dafny
5(1)
0.3 Other Languages
6(3)
Part 0 Learning the Ropes
1 Basics
9(16)
1.0 Methods
9(1)
1.1 Assert Statements
10(1)
1.2 Working with the Verifier
11(1)
1.3 Control Paths
12(1)
1.4 Method Contracts
13(4)
1.5 Functions
17(2)
1.6 Compiled versus Ghost
19(2)
1.7 Summary
21(4)
2 Making It Formal
25(38)
2.0 Program State
26(2)
2.1 Floyd Logic
28(1)
2.2 Hoare Triples
29(3)
2.3 Strongest Postconditions and Weakest Preconditions
32(8)
2.4 WP and SP
40(1)
2.5 Conditional Control Flow
41(4)
2.6 Sequential Composition
45(1)
2.7 Method Calls and Postconditions
46(4)
2.8 Assert Statements
50(3)
2.9 Weakest Liberal Preconditions
53(2)
2.10 Method Calls with Preconditions
55(2)
2.11 Function Calls
57(1)
2.12 Partial Expressions
58(2)
2.13 Method Correctness
60(1)
2.14 Summary
60(3)
3 Recursion and Termination
63(20)
3.0 The Endless Problem
64(2)
3.1 Avoiding Infinite Recursion
66(4)
3.2 Well-Founded Relations
70(2)
3.3 Lexicographic Tuples
72(7)
3.4 Default decreases in Dafny
79(1)
3.5 Summary
80(3)
4 Inductive Datatypes
83(12)
4.0 Blue-Yellow Trees
84(1)
4.1 Matching on Datatypes
85(1)
4.2 Discriminators and Destructors
86(2)
4.3 Structural Inclusion
88(1)
4.4 Enumerations
89(1)
4.5 Type Parameters
89(1)
4.6 Abstract Syntax Trees for Expressions
90(3)
4.7 Summary
93(2)
5 Lemmas and Proofs
95(42)
5.0 Declaring a Lemma
96(1)
5.1 Using a Lemma
96(3)
5.2 Proving a Lemma
99(3)
5.3 Back to Basics
102(4)
5.4 Proof Calculations
106(4)
5.5 Example: Reduce
110(5)
5.6 Example: Commutativity of Multiplication
115(3)
5.7 Example: Mirroring a Tree
118(4)
5.8 Example: Working on Abstract Syntax Trees
122(8)
5.9 Summary
130(7)
Part 1 Functional Programs
6 Lists
137(24)
6.0 List Definition
137(1)
6.1 Length
138(1)
6.2 Intrinsic versus Extrinsic Specifications
139(3)
6.3 Take and Drop
142(2)
6.4 At
144(2)
6.5 Find
146(1)
6.6 List Reversal
147(4)
6.7 Lemmas in Expressions
151(6)
6.8 Eliding Type Arguments
157(1)
6.9 Summary
158(3)
7 Unary Numbers
161(14)
7.0 Basic Definitions
162(1)
7.1 Comparisons
162(3)
7.2 Addition and Subtraction
165(2)
7.3 Multiplication
167(1)
7.4 Division and Modulus
167(5)
7.5 Summary
172(3)
8 Sorting
175(14)
8.0 Specification
175(4)
8.1 Insertion Sort
179(2)
8.2 Merge Sort
181(7)
8.3 Summary
188(1)
9 Abstraction
189(18)
9.0 Grouping Declarations into Modules
190(1)
9.1 Module Imports
190(1)
9.2 Export Sets
191(3)
9.3 Modular Specification of a Queue
194(7)
9.4 Equality-Supporting Types
201(3)
9.5 Summary
204(3)
10 Data-Structure Invariants
207(28)
10.0 Priority-Queue Specification
208(2)
10.1 Designing the Data Structure
210(2)
10.2 Implementation
212(12)
10.3 Making Intrinsic from Extrinsic
224(5)
10.4 Summary
229(6)
Part 2 Imperative Programs
11 Loops
235(22)
11.0 Loop Specifications
235(6)
11.1 Loop Implementations
241(6)
11.2 Loop Termination
247(3)
11.3 Summarizing the Loop Rule
250(2)
11.4 Integer Square Root
252(3)
11.5 Summary
255(2)
12 Recursive Specifications, Iterative Programs
257(18)
12.0 Iterative Fibonacci
257(3)
12.1 Fibonacci Squared
260(4)
12.2 Powers of 2
264(3)
12.3 Sums
267(5)
12.4 Summary
272(3)
13 Arrays and Searching
275(46)
13.0 About Arrays
275(5)
13.1 Linear Search
280(8)
13.2 Binary Search
288(4)
13.3 Minimum
292(2)
13.4 Coincidence Count
294(7)
13.5 Slope Search
301(3)
13.6 Canyon Search
304(5)
13.7 Majority Vote
309(9)
13.8 Summary
318(3)
14 Modifying Arrays
321(16)
14.0 Simple Frames
321(5)
14.1 Basic Array Modification
326(10)
14.2 Summary
336(1)
15 In-situ Sorting
337(14)
15.0 Dutch National Flag
337(4)
15.1 Selection Sort
341(2)
15.2 Quicksort
343(4)
15.3 Summary
347(4)
16 Objects
351(36)
16.0 Checksums
352(7)
16.1 Tokenizer
359(5)
16.2 Simple Aggregate Objects
364(10)
16.3 Full Aggregate Objects
374(8)
16.4 Summary
382(5)
17 Dynamic Heap Data Structures
387(40)
17.0 Lazily Initialized Arrays
387(9)
17.1 Extensible Array
396(7)
17.2 Binary Search Tree for a Map
403(10)
17.3 Iterator for the Map
413(10)
17.4 Summary
423(4)
A Dafny Syntax Cheat Sheet
427(6)
B Boolean Algebra
433(12)
B.0 Boolean Values and Negation
433(1)
B.1 Conjunction
433(1)
B.2 Predicates and Well-Definedness
434(1)
B.3 Disjunction and Proof Format
435(2)
B.4 Implication
437(1)
B.5 Proving Implications
438(1)
B.6 Free Variables and Substitution
439(2)
B.7 Universal Quantification
441(1)
B.8 Existential Quantification
442(3)
C Answers to Select Exercises
445(14)
References 459(8)
Index 467