COMP 401 ASSERTIONS Instructor Prasun Dewan ASSERTIONS Declare some property of the program Potentially useful for specification testing formal correctness documentation user interface automation 2 COMPILE TIME VS RUNTIME PROPERTIES Some assertions are language supported Compile time String s nextElement Runtime String nextElement We will consider runtime properties Casting is application independent 3 APPLICATION INDEPENDENT VS DEPENDENT Language can provide us with fixed number of application independent assertions Cannot handle First character of String is a letter Letter concept not burnt into language Class Character defines it Innumerable assertions about letters possible Second elements of string is letter Third element of string is letter Need mechanism to express arbitrary assertions Originally Java had no assertions In 1 4 assertions were added 4 JAVA ASSERTIONS PRE POST CONDITIONS assert Boolean Expression assert Boolean Expression Value Statement can be inserted anywhere to state that some condition should be true If condition is false Java throws AssertionError which may be caught by programmer code If uncaught depending on which assert used generic message saying assertion failed printed Value toString printed An assertion made at the beginning end of a statement block method loop if is called its precondition postcondition 5 PREVENTING INVALID BMI 6 HOW SHOULD WE CHANGE THE CLASS public class ABMISpreadsheet double height weight public ABMISpreadsheet double theInitialHeight double theInitialWeight setHeight theInitialHeight setWeight theInitialWeight public double getHeight return height public void setHeight double newHeight height newHeight public double getWeight return weight public void setWeight double newWeight weight newWeight public double getBMI return weight height height 7 CHECKING PRECONDITIONS public class ABMISpreadsheet double height weight public ABMISpreadsheet double theInitialHeight double theInitialWeight setHeight theInitialHeight setWeight theInitialWeight public boolean preGetBMI return weight 0 height 0 public double getBMI assert preGetBMI return weight height height Precondition of method M is preM ObjectEditor does not call M if preM is false 8 OBJECTEDITOR USES PRECONDITIONS 9 OBJECTEDITOR USES PRECONDITION 10 OBJECTEDITOR USES PRECONDITION The menu item for a method is disabled when its precondition not met 11 NEW CLASS public class ABMISpreadsheet double height weight double initialHeight initialWeight public ABMISpreadsheet double theInitialHeight double theInitialWeight setHeight theInitialHeight setWeight theInitialWeight initialHeight theInitialHeight initialWeight theInitialWeight public boolean preGetBMI return weight 0 height 0 public double getBMI assert preGetBMI return weight height height public boolean preRestoreHeightAndWeight return height initialHeight weight initialWeight public void restoreHeightAndWeight assert preRestoreHeightAndWeight height initialHeight weight initialWeight 12 PRECONDITIONS OF OTHER METHODS public class ABMISpreadsheet public double getWeight return weight public void setWeight double newWeight weight newWeight 13 PRECONDITIONS OF OTHER METHODS public class ABMISpreadsheet public double preGetWeight return weight 0 public double getWeight assert preGetWeight return weight public boolean preSetWeight double newWeight return newWeight 0 public void setWeight double newWeight assert preSetWeight newWeight weight newWeight Prevention of getter not needed if setter and constructor prevent assignment of illegal values 14 EQUIVALENT CLASS public class ABMISpreadsheet public double getWeight return weight public boolean preSetWeight double newWeight return newWeight 0 public void setWeight double newWeight assert preSetWeight newWeight weight newWeight Prevention of getter not needed if setter and constructor prevent assignment of illegal values 15 PRECONDITION STYLE RULE If there are constraints on the input of a method M that may not be met write a precondition boolean method preM for it Call the precondition method in an assert statement as the first statement of M To keep examples short preconditions will not be shown in future examples 16 EXPRESSING ASSERTIONS Natural No language collection element is null All collection elements are not odd All collection elements are either odd or positive Easy to read but ambiguous Programming Library language or language constructs Executable unambiguous but language dependent and awkward Useful for debugging Specification cannot be done before language decided Mathematical language Unambiguous time tested convenient but not executable j 0 j b size b get j null 17 PROPOSITIONAL CALCULUS Logic operators not and or We will use Java syntax Quantifiers Universal Existential Propositional j 0 j b size b get j null b get j a get 0 variables Program Others Recording Quantifier Propositions Boolean expressions involving operators variables and quantifiers Simple quantified Do propositions not use use quantifiers 18 PROPOSITIONAL ALGEBRA Calculus based on algebra Algebra defines Arithmetic operations Relations operations We will use Java syntax j 0 j b size b get j null b get j a get 0 19 EXAMPLE PROPOSITIONS Simple True propositions False weight 0 weight 0 height 0 Quantified j All elements of B are not null j 0 j b size b get j null 0 j b size b get j null At least one element of B is not null 20 QUANTIFIED PROPOSITIONS Quantified j 0 j b size b get j null j 0 j b size b get j null General form Qx D x P x Q is either or quantifier X is quantified variable D x is domain description P x is sub proposition Sub proposition Simple or quantified proposition in terms of quantifier Domain A collection of values used in sub proposition evaluation b get 0 b get b size 1 Domain description Describes domain using quantified variable 21 QUANTIFIED ASSERTIONS Syntax Qx D x P x 0 j b size b get j null j 0 j b size b get j null j Goal Write general boolean functions that take as arguments encoding of the elements of domain and return true iff proposition is true 22 EXPRESSING QUANTIFIED ASSERTIONS public interface Asserter public boolean checkQuantified String assertion Library must do parsing Cannot pass expression string as variables such as b in our scope have no meaning to library Qx D x P x j 0 j b size b get j null assert asserter checkQuantified j 0 j b size b get j null some element of b is null 23 SEPARATE THE THREE COMPONENTS public interface Asserter public boolean