Predicate Logic for Software Engineering David Lorge Parnas McMaster University Ontario Canada Presentation for SwE Readings Class By Sridhar Pentapati About Dave Parnas His insights have changed the way that we specify design document build and maintain software His techniques have changed modern programming languages His wisdom has steered software engineering field 03 21 03 Sri Progress in a scientific discipline can be measured by how quickly its founders are forgot ten 3 Abstract 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 03 21 03 Sri Logic is in the eye of the logician Gloria Steinem 4 Introduction Predicate logic is a development of propositional logic which we re all well acquainted with Sentences in predicate calculus are built up from atomic sentences 03 21 03 Contrariwise continued Tweedledee if it was so it might be and if it were so it would be 5 but as it isn t it ain t That s logic Lewis Carroll Introduction contd Why logic in SwE 1 Engineers need mathematical tools 1 for the description and analysis of their products 2 Mathematical logic is the basis of all proposed tools 1 A solid foundation of logic notation will be essential for anyone who hopes to be recognized as a software engineer 03 21 03 Sri Predicate Logic For Software Engineering 6 Introduction Contd Focus It is essential to have a precise meanings for logical expressions one that unambiguously yields a value of true or false for every statement of values to the variables that appear in an expression 03 21 03 Sri Logic is one thing the human animal another You can quite easily propose a logical solut 7 ion to something and at the same time hope in your heart of hearts it won t work out Lu Problems with Existing Logic Logicians are conservative Believes Martin Van Emden 2 Lacks precise meaning for logical expression values 3 Complexity of expressions 4 Assumption of total functions 1 03 21 03 Sri Logic The art of thinking and reasoning in strict accordance with the limitations and in capacities of the human misunderstanding Ambrose Bierce 8 Parnas Says Change predicate logic to allow functions to be partial 2 To do away with the resulting truth value undefined 1 03 21 03 Sri The want of logic annoys Too much logic bores Life eludes logic and everything that log 9 ic alone constructs remains artificial and forced Andr Gide Structure of The Paper 1 2 3 4 5 6 7 Introduction Basic definitions Syntax of Logic Expressions Meanings of Logical Expressions Examples of the Use of This Logic in Software Documentation Conclusions References 03 21 03 Sri Predicate Logic For Software Engineering 10 Reasons and Goal Since practitioners do not want to use methods that require them to use many symbols to say simple things They will not read expressions that are lengthy or deeply nested A full formal definition of a logic that permits concise expressions is a prerequisite for practical use 03 21 03 Sri The fact that logic cannot satisfy us awakens an almost insatiable hunger for the irrational 11 A N Wilson Introduction contd In one of his earlier papers Parnas reminded us that 1 functions and relations can be viewed as sets of ordered pairs 2 sets can be characterized by predicates and described by logical expressions 3 predicates can be represented in more readable way using multidimensional expressions and 4 the meaning of these tables can be defined by rules for translating those tables into more conventional expressions 03 21 03 Sri Predicate Logic For Software Engineering 12 Introduction Contd Many researchers are developing mathematical methods for use by software developers It is hoped that these methods would do for SwE what differential and integral calculus did for other areas of engineering 03 21 03 Sri From a drop of water a logician could infer the possibility of an Atlantic or a Niagara wi thout having seen or heard of one or the other Sir Arthur Conan Doyle 13 Introduction contd Crux of the problem 1 2 Conventional formal interpretations of logical expressions e g Mendelson 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 value has not been defined for certain values of the argument 03 21 03 Sri Predicate Logic For Software Engineering 14 Basics A partial function from a set A to a set B is an assignment to each element a in a subset of A called the domain of definition of of a unique element b in B The sets A and B are called the domain and codomain of respectively 03 21 03 Sri Predicate Logic For Software Engineering 15 Basics Contd We say that is undefined for elements in A that are not in the domain of definition of We write A B to denote that is a partial function from A to B When the domain of definitions equals A we say that is a total function 03 21 03 Sri Logic is like the sword those who appeal to it shall perish by it Samuel Butler 16 Another interpretation of Predicate Expressions But why Since under conventional interpretations a logical expression that includes partial functions will have a defined value only when the values assigned to all function arguments are within functions domains Such interpretations are of limited usefulness when describing software because we frequently use partial functions to describe the behavior of programs 03 21 03 Sri Predicate Logic For Software Engineering 17 Motivating Example Assume that represents a function that is defined on a domain containing only non negative real numbers A s w designer may write a boolean expression such as x 0 y x x 0 y x 1 to describe the behavior of a computer program 03 21 03 Sri Predicate Logic For Software Engineering 18 The writer s intent seems to be to write an expression that is equivalent to y x 2 the usual rules for evaluating such expressions require evaluation of all of the functions and relational operators before application of the logical operators to the truthvalues that result For every value of x other than 0 19 03 21 03 Sri Predicate Logic For Software Engineering Comparison with Other Work There is a huge and complex literature on the subject of logic with partial functions This paper presents a specific proposal and its