Predicate Logic for Software Engineering



Predicate Logic for Software Engineering

- by David Lorge Parnas

CSc 79000: Software Engineering – Readings in Computer Science

Professor Danny Kopec

Summary by: Sridhar Pentapati

The interpretations of logical expressions found in most of the introductory textbooks are not suitable for use in software engineering applications because they do not deal with partial functions. More advanced papers and texts deal with partial functions in a variety of complex ways. This paper proposes a very simple change to the classic interpretation of predicate expressions, one that defines their value for all values of all variables, yet is almost identical to the standard definitions. It then illustrates the application of this interpretation in software documentation.

Parnas goes about this in a structured way: Basic definitions, Syntax of Logical Expressions, Meaning of Logical Expressions, Examples of the Use of Predicate Logic in Software Documentation, and Conclusions.

Professional engineers can often be distinguished from other designers by the engineers’ ability to use mathematical methods to describe and analyze their products. A solid understanding of mathematical logic would be essential for anyone to be recognized as a software engineer.

This paper focuses greatly on the importance of partial functions in the software documentation. Parnas gives a mathematical way of denoting predicates, so that they behave like total functions. In software development it is of paramount importance to have an accurate meaning for logical expressions, one that unambiguously gives a value true or false for every assignment of values to the variables that appear in an expression.

Software engineers are interested in concise and intuitively appealing presentations of specifications of conditions with many different cases: if necessary, page upon page of tables. They were interested in specifying, and executing, theories taking up many pages. The logic of logic was never intended for practical applications. Their formulas are toy formulas. Software engineers should follow the example of logic programmers and define a version of logic suited for their specific, practical purposes. Parnas’ paper is a pioneering step in this direction.

The most conventional formal interpretations of logical expressions assume that all functions are total, i.e., defined on a domain that includes all possible values of their arguments. Those interpretations are not intended to deal with partial functions, functions whose values have not been defined for certain values of the arguments. Under conventional interpretations, a logical expression that includes partial functions will have a defined value only if the values assigned to the arguments of each function are within that function’s domain. In essence, the predicate defined by the expression is partial. Such interpretations are of limited use when describing software because we frequently use partial functions to describe the behavior of programs.

This paper is concerned with the difficulty exemplified by defining logic [pic] without using the absolute function. It seems okay, but ((x > 0) ( (y =[pic])) ( ((x ( 0) ( (y = [pic])) does not work, as the left part of the disjunction is not defined when x is negative, while the right part of the disjunction is undefined when x is positive. Parnas solves this by defining a new system of logic.

A predicate is a characteristic or attribute or property that the subject of the statement can have. Predicate logic allows us to represent fairly complex facts about the world, and to derive new facts in a way that guarantees that, if the initial facts were true then so are the conclusions. It is a well-understood formal language, with well-defined syntax, semantics and rules of inference.

Conclusions:

1. Not necessary to introduce either a third variable or conditional operators in order to

deal with partial functions.

2. Not only is the “motivating example” eq (1) fully defined using the set-theoretic

operations but also greatly simplified:

(y =[pic]) ( (y =[pic])

This form which has no “guarding” expressions, has exactly the same denotation as

the one shown earlier.

3. Compact readable formulation is crucial.

4. Easier to comprehend.

5. Drawbacks with some complementary predicates – price for allowing partial functions

6. The properties of the functions used should be stated precisely.

7. Axiom of reflection does not hold in this interpretation.

8. Simplification is obtained by making primitive predicates evaluate to false whenever

one or more of their arguments are undefined.

Parnas believes that these are proper decisions because:

1. Keeping logic simple is essential to practical application.

2. The assigned meanings are consistent with intuitive interpretations, and

3. The formulae that results are relatively simple for cases arising frequently.

................
................

In order to avoid copyright disputes, this page is only a partial summary.

Google Online Preview   Download