Rigorous Software Development | springerprofessional.de

Springer Professional

nach oben

2011 | Buch

Kapitel lesen Erstes Kapitel lesen

Rigorous Software Development

An Introduction to Program Verification

verfasst von: José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa

Verlag: Springer London

Buchreihe : Undergraduate Topics in Computer Science

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

Einloggen, um Zugang zu erhalten

Über dieses Buch

The use of mathematical methods in the development of software is essential when reliable systems are sought; in particular they are now strongly recommended by the official norms adopted in the production of critical software. Program Verification is the area of computer science that studies mathematical methods for checking that a program conforms to its specification. This text is a self-contained introduction to program verification using logic-based methods, presented in the broader context of formal methods for software engineering. The idea of specifying the behaviour of individual software components by attaching contracts to them is now a widely followed approach in program development, which has given rise notably to the development of a number of behavioural interface specification languages and program verification tools. A foundation for the static verification of programs based on contract-annotated routines is laid out in the book. These can be independently verified, which provides a modular approach to the verification of software. The text assumes only basic knowledge of standard mathematical concepts that should be familiar to any computer science student. It includes a self-contained introduction to propositional logic and first-order reasoning with theories, followed by a study of program verification that combines theoretical and practical aspects - from a program logic (a variant of Hoare logic for programs containing user-provided annotations) to the use of a realistic tool for the verification of C programs (annotated using the ACSL specification language), through the generation of verification conditions and the static verification of runtime errors.

Anzeige

Inhaltsverzeichnis

Frontmatter

Chapter 1. Introduction

Abstract

The first chapter introduces the notion of rigourous software development in the context of the classic software development methods used in software engineering. The rigorous aspect in particular, which is properly contextualised and justified in this chapter, is here introduced as the result of following a formal approach, by which we mean the use of tools and methods of a mathematical nature.

In order to allow the reader to understand their value, these methods are compared, throughout the chapter, with more traditional methods such as testing and simulation, and placed in the normative context in use in the different application areas of software engineering.

José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa

Chapter 2. An Overview of Formal Methods Tools and Techniques

Abstract

The goal of this chapter is to give an overview of the different approaches and tools pertaining to formal methods. We do not attempt to be exhaustive, but focus instead on the main approaches (formal specification, formal verification and proofs, transformation, and formal development). A consise introduction to basic logic concepts and methods is also provided. After reading the chapter the reader will be familiar with the terminology of the area, as well as with the most important concepts and techniques.

Moreover the chapter will allow the reader to contextualise and put into perspective the topics that are covered in detail in the book.

José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa

Chapter 3. Propositional Logic

Abstract

Propositional logic is the basis for any study of logic. The sentences of propositional logic are built from a set of unstructured atomic propositions that are combined using a number of logical connectives. Logical connectives are Boolean operators whose names come from natural language, such as “not”, “and”, “or” and “implies”, and they are given a formal meaning that mimics its usage in natural language.

This chapter is devoted to the study of classical propositional logic. The chapter starts with a presentation of both the syntax and the semantics of propositional logic. In other words, we describe both the set of sentences of the language of propositional logic, and characterise the meaning of those sentences (i.e. which sentences are valid or not). The notion of proof derivation is then introduced as a syntactic characterisation of logical inference, and the interplay between provability and validity is established. The chapter concludes with a discussion of the decision problem of checking whether a propositional formula is valid or not.

José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa

Chapter 4. First-Order Logic

Abstract

First-order logic augments the expressive power of propositional logic as it links the logical assertions to properties of objects of some non-empty universe: the domain of discourse. This is achieved by allowing the propositional symbols to take arguments that range over elements of the domain of discourse. These are now called predicate symbols and are interpreted as relations on the domain. Elements of the domain of discourse are denoted by terms built up from variables, constants, and functions applied to other terms. First-order logic also expands the lexicon of propositional logic with the quantifiers “for all” and “there exists” that are interpreted consistently with their natural language meaning.

This chapter is devoted to classical first-order logic. Our presentation is similar to the one conducted for propositional logic. We first define the syntax of first-order logic, followed by its semantics. Next we define a proof system for it and present the fundamental theoretical results of soundness and completeness. We also discuss the decision problems related to this logic. The remaining sections of the chapter cover variations and extensions of first-order logic, as well as first-order theories.

José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa

Chapter 5. Hoare Logic

Abstract

Hoare logic is the fundamental formalism introduced by C.A.R. Hoare in 1969 for reasoning about the correctness of imperative programs, building on first-order logic. In this chapter we study a program logic which is a variant of Hoare logic for programs containing user-provided annotations.

The logic deals with the notion of correctness vis a vis a specification that consists of a precondition and a postcondition. The correctness of a program with respect to a given specification is asserted by constructing a derivation in the inference system of Hoare logic. While doing so, one must identify an invariant for every loop in the program.

This chapter also discusses the important problem of adaptation of specifications, since it has major implications on the design of practical verification systems based on Hoare logic.

José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa

Chapter 6. Generating Verification Conditions

Abstract

In this chapter we consider the problem of mechanising the construction of derivations in Hoare logic having a given Hoare triple as conclusion. We are thus concerned with the backwards application of rules of the logic, which will eventually produce a derivation, i.e. a tree in which all leaves correspond to instances of axioms, and all side conditions hold.

The goal of this chapter is to show that there exists a strategy for conducting the proofs such that, if some of the side conditions required do not hold, then no derivation exists for the goal at hand. This strategy results in the definition of what is usually known as a verification conditions generator.

José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa

Chapter 7. Safety Properties

Abstract

This chapter considers a method for dealing statically with the occurrence of errors during the execution of programs. Recall that to this point we have been considering that evaluation of an expression could never go wrong, and neither could the execution of a command.

This is clearly unsatisfying since in real-world languages runtime errors do occur, and one of the main uses of verification methods is precisely to ensure the safety of programs, i.e. the absence of such error situations. This chapter presents a general framework for reasoning with errors and safety.

José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa

Chapter 8. Procedures and Contracts

Abstract

The presence of sub-routines is as important as it is challenging from the point of view of verification. In this chapter we study a form of program logic that is adequate for reasoning about programs with procedures, and moreover it is adequate for motivating the principles that are used in practice by program verification tools and standard annotation languages, as illustrated in Chaps. 9 and 10. The material studied in the present chapter covers the interprocedural level, but at the intraprocedural level the code in the body of procedures still needs to be verified; the inference systems presented in this chapter are thus meant as extensions of systems studied previously.

The chapter starts with an overview of some of the issues involved in reasoning about procedures. Subsequent sections cover in turn inference rules and verification conditions for programs consisting of mutually recursive parameterless procedures; frame conditions; procedures with parameters; and finally return values and functions.

José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa

Chapter 9. Specifying C Programs

Abstract

In this chapter we shift the focus of our study to programs written in a realistic programming language. In particular, we focus on the ANSI/ISO C Specification Language (ACSL), which is an annotation language for C programs. ACSL has scope for frame conditions, loop invariants and variants, predicates and logic functions (either defined or specified by axioms), and a state label mechanism.

In the previous chapter we have introduced contracts and the principles of contract-based verification. ACSL adheres to these principles: each C function in a program is annotated with an ACSL specification—the function’s contract. Verification of a program consisting of a number of mutually-recursive functions is completely modular: each function is verified against its own contract, assuming that all other functions are correct. The program is correct if all functions are correct.

José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa

Chapter 10. Verifying C Programs

Abstract

In this chapter we study a verification tool, called Frama-C, for ACSL-annotated C programs. In fact Frama-C is much more than a verification tool: it is a general, plug-in-based program analysis tool, designed to be used in practice in industrial projects. The program verification functionality of Frama-C used in the present chapter is provided by the Jessie plug-in. Jessie in turn relies on the use of a multi-prover VCGen tool that can export verification conditions to many different proof tools, including for instance the Simplify and Z3 automatic provers, and proof assistants like Coq.

Our approach in the present chapter is to start from an algorithm for which only an informal specification is given. We annotate the C code of this function as we go along, starting with the minimal annotations required for verification of safety, followed later by other functional properties.

José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa

Backmatter

Titel: Rigorous Software Development
verfasst von: José Bacelar Almeida
Maria João Frade
Jorge Sousa Pinto
Simão Melo de Sousa
Copyright-Jahr: 2011
Verlag: Springer London
Electronic ISBN: 978-0-85729-018-2
Print ISBN: 978-0-85729-017-5
DOI: https://doi.org/10.1007/978-0-85729-018-2

Premium Partner