Predicate Logic for Software Engineering

Summary for Class 1/18/2019

Predicate Logic for Software Engineering

- by David Lorge Parnas

CSc 79000: Software Engineering – Readings in Computer Science

Professor Danny Kopec

Summary by: Sridhar Pentapati

Conventional interpretations of expressions that describe predicates are not suitable for use in software engineering because they do not deal with partial functions. Parnas’ team defines an interpretation for predicate expressions that is suitable for use 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.

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.

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 has 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 without using the absolute function. It seems okay, but ((x > 0)  (y =))  ((x  0)  (y = )) 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.

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 =)  (y =)

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.

1