Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben

2007 | Buch

Propositional Logic Kapitel lesen Erstes Kapitel lesen

The Calculus of Computation

Decision Procedures with Applications to Verification

verfasst von: Aaron R. Bradley, Zohar Manna

Verlag: Springer Berlin Heidelberg

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

Computational logic is a fast-growing field with applications in artificial intelligence, constraint solving, and the design and verification of software and hardware systems. Written with graduate and advanced undergraduate students in mind, this textbook introduces computational logic from the foundations of first-order logic to state-of-the-art decision procedures for arithmetic, data structures, and combination theories.

This textbook also presents a logical approach to engineering correct software. The increasing ubiquity of computers makes implementing correct systems more important than ever. Verification exercises develop the reader's facility in specifying and verifying software using logic. The treatment of verification concludes with an introduction to the static analysis of software, an important component of modern verification systems.

For readers interested in learning more about computational logic, decision procedures, verification, and other areas of formal methods, the final chapter outlines courses of further study.

Inhaltsverzeichnis

Frontmatter

Foundations

Frontmatter
1. Propositional Logic
Abstract
A calculus is a set of symbols and a system of rules for manipulating the symbols. In an interesting calculus, the symbols and rules have meaning in some domain that matters. For example, the differential calculus defines rules for manipulating the integral symbol over a polynomial to compute the area under the curve that the polynomial defines. Area has meaning outside of the calculus; the calculus provides the tool for computing such quantities. The domain of the differential calculus, loosely speaking, consists of real numbers and functions over those numbers.
2. First-Order Logic
Abstract
This chapter extends the machinery of propositional logic to first-order logic (FOL), also called both predicate logic and the first-order predicate calculus. While first-order logic enjoys a degree of expressiveness that makes it suitable for reasoning about computation, it does not admit completely automated reasoning.
3. First-Order Theories
Abstract
When reasoning in particular application domains such as software or hardware, one often has particular structures in mind. For example, programs manipulate numbers, lists, and arrays. First-order theories formalize these structures to enable reasoning about them. This chapter introduces first-order theories in general and then focuses on theories useful in verification and related tasks. These theories include a theory of equality, of integers, of rationals and reals, of recursive data structures, and of arrays.
4. Induction
Abstract
This chapter discusses induction, a classic proof technique for proving first-order theorems with universal quantifiers. Section 4.1 begins with stepwise induction, which may be familiar to the reader from earlier education. Section 4.2 then introduces complete induction in the context of arithmetic. Complete induction is theoretically equivalent in power to stepwise induction but sometimes produces more concise proofs. Section 4.3 generalizes complete induction to well-founded induction in the context of arithmetic and recursive data structures. Finally, Section 4.4 covers a form of well-founded induction over logical formulae called structural induction. It is useful for reasoning about correctness of decision procedures and properties of logical theories and their interpretations.
5. Program Correctness: Mechanics
Abstract
We are finally ready to apply FOL and induction to a real problem: specifying and proving properties of programs. In this chapter, we develop the three foundational methods that underly all verification and program analysis techniques. In the next chapter, we discuss strategies for applying them.
6. Program Correctness: Strategies
Abstract
As in other applications of mathematical induction (see Example 4.1), the main challenge in applying the inductive assertion method is discovering extra information to make the inductive argument succeed. Consider a typical partial correctness property that asserts that a function’s output satisfies some relation with its input. Assuming this property as the inductive hypothesis does not provide any information about how the function behaves between entry and exit. It is a weak hypothesis. Therefore, one must provide more information about the function in the form of additional program annotations. Section 6.1 discusses strategies for discovering this additional information. Section 6.2 applies the strategies to prove that QuickSort always returns a sorted array.

Algorithmic Reasoning

Frontmatter
7. Quantified Linear Arithmetic
Abstract
Recall from Chapter 3 that satisfiability in the theories of linear integer arithmetic T ℤ and linear rational (or real) arithmetic T ℚ is decidable. This chapter explores a common method of deciding satisfiability of arbitrarily quantified formulae in decidable theories in the context of T ℤ and T ℚ.
8. Quantifier-Free Linear Arithmetic
Abstract
This chapter considers satisfiability in the quantifier-free fragment of the theory of rationals T ℚ. Addressing this fragment is motivated by two observations. First, program verification typically requires just considering formulae from the quantifier-free fragments of theories such as T ℚ. Second, deciding satisfiability in the full theory of T ℚ is computationally expensive, while deciding satisfiability in just the quantifier-free fragment of T ℚ is fast in practice when using, for example, the simplex method for linear programming.
9. Quantifier-Free Equality and Data Structures
Abstract
Equality is perhaps the most widely-used relation among data in programs. In this chapter, we consider equality among variables, constants, and function applications (Section 9.1); among recursive data structures (records, lists, trees, and stacks) and their elements (Section 9.4); and among elements of arrays (Section 9.5). For all three theories, we examine their quantifier-free fragments.
10. Combining Decision Procedures
Abstract
Chapters 7–9 consider decision procedures for theories that each formalize just one data type. Yet almost all formulae in Chapter 5 are formulae of union theories. For example, many assert facts in T ℚ ∪ T A about arrays of integers indexed by integers. Additionally, the decision procedure for the array property fragment of T A ℚ that we discuss in Chapter 11 requires a procedure for the quantifier-free fragment of T ℚ ∪ T A. Can we reuse the decision procedures of Chapters 7–9 to decide satisfiability of formulae in union theories, or must we invent a new procedure for each combination?
11. Arrays
Abstract
Programs rely on data structures to store and manipulate data in complex ways. Therefore, verifying these programs requires decision procedures that reason about the data structures. This chapter discusses fragments and decision procedures for reasoning about arrays and array-like data structures: arrays with anonymous or uninterpreted indices (Section 11.1), the familiar arrays of C and other imperative languages with integer indices (Section 11.2), and hashtables (Section 11.3).
12. Invariant Generation
Abstract
While applying the inductive assertion method of Chapters 5 and 6 certainly requires insights from the programmer, algorithms that examine programs can discover many simple properties. This chapter describes a form of static analysis called invariant generation, whose task is to discover inductive assertions of programs. A static analysis is a procedure that operates on the text of a program. An invariant generation procedure is a static analysis that produces inductive program annotations as output.
13. Further Reading
Abstract
In this book we have presented a classical method of specifying and verifying sequential programs (Chapters 5 and 6) based on first-order logic (Chapters 1–3) and induction (Chapter 4). We then focused on algorithms for automating the application of this method: decision procedures for reasoning about verification conditions (Chapters 7–11), and invariant generation procedures for deducing inductive facts about programs (Chapter 12). This material is fundamental to all modern research in verification. In this chapter, we indicate topics for further reading and research.
Backmatter
Metadaten
Titel
The Calculus of Computation
verfasst von
Aaron R. Bradley
Zohar Manna
Copyright-Jahr
2007
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-540-74113-8
Print ISBN
978-3-540-74112-1
DOI
https://doi.org/10.1007/978-3-540-74113-8

Premium Partner

    Bildnachweise