Method Verification
Explore the process of verifying methods in software development, covering concepts such as verification vs. validation, contract verification, and maintaining the representation invariant. Learn how to analyze and verify methods in isolation, ensuring correctness and reliability in your code.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Method Verification Paul Ammann
Verification vs Validation Verification vs. Validation Verification A given implementation is correct with respect to another description Validation A given description is desirable We will focus on Verification in this lecture Good news! All Verification Obligations follow the same basic model! 2
Verification of Method Contracts in Data Abstractions First basic problem Contract is in JavaDoc Code is in Java How are the states related? Solution: Abstraction Function maps Representation States to Abstract States 3
Key to verifying methods in isolation Common (flawed) informal approach to analyzing a given method: See how other methods behave Worry about method interactions Interactions are reflected in representation state. This doesn t scale! Instead, we want to analyze each method by itself We need a general description of important properties relevant to all methods Exactly what the Rep Invariant does 4
Method Verification: Part 1 The Representation Invariant Does the method establish/maintain the rep-invariant? Base case for constructors Plus any other methods that create objects Clone? Serialization? Inductive case for mutators 5
Method Verification Part 2: The Contract Given The Rep Invariant as an Assumption Given Preconditions as Assumptions Does the Postcondition Hold? Need to Map States Through Abstraction Function 6
Verification In Diagram Form Abstract State (Before) Abstract State (After) Method ? Contract AF() AF() Representation State (After) Representation State (Before) Method Code 7
Verification Example Diagram shown for method verification Will revisit same diagram for overridden methods Example to develop in class: public class Members { // Members is a mutable record of organization membership // AF: ?? // rep-inv: ?? List<Person> members; // the representation // Post: person becomes a member public void join (Person person) { members.add (person);} // Post: person is no longer a member public void leave(Person person) { members.remove(person);} } Exactly what is incorrect? Verification tools: Contract, Abstraction function, Representation Invariant Validation question: What about null values in members? 8
Verification Example - Analysis rep-inv: members != null && no duplicates in members rep-inv: members != null join() Maintain rep-inv? Yes Satisfy contract? Yes leave() Maintain rep-inv? Yes Satisfy contract? No join() Maintain rep-inv? No Satisfy contract? Not a meaningful question leave() Maintain rep-inv? Yes Satisfy contract? Yes 9
Verification Example Repair 1 rep-inv: members != null Analysis join() join() Maintain rep-inv? Yes already analyzed Satisfy contract? Yes already analyzed leave() Maintain rep-inv? Yes Satisfy contract? Yes As is leave() while (members.contains(person)) { members.remove(person); } 10
Verification Example Repair 2 rep-inv: members != null && no duplicates in members Analysis join() if (!members.contains(person)) { members.add(person); { leave() join() Maintain rep-inv? Yes Satisfy contract? Yes leave() Maintain rep-inv? Yes Already analyzed Satisfy contract? Yes Already analyzed As is 11
Another Verification Example public class Poly { // Polys are immutable polynomials c0 + c1x + c2x^2 + // AF: ci = trms[i] for appropriate values of i // rep-inv: deg = trms.length-1 // trms.length >= 1 // trms != null // if deg > 0 then trms[deg] != 0 int[] trms; int deg; // the representation // Post: Return degree of this, ie largest exponent with // coefficient != 0. Returns 0 if this is zero Poly public int degree() { return deg; } // Other methods omitted } How do we decide if degree() is correct? How must code change if rep-inv changes? 12
