Software Design and Construction 2 SOFT3202 / COMP9202 Design Verification & Test Driven Development
Prof Bernhard Scholz School of Computer Science
The University of Sydney
Page 1
Agenda
– DesignVerification
– OCL
– Alloy
– TestDrivenDevelopment
The University of Sydney
Page 2
Design Verification
– Quest:howtotestthatthedesigniscorrect?
– Forcode:useunit/integration/system/acceptancetestsand
regression tests for changes.
– Fordesign:nothingtoexecute;testingadesignishard
– Howcanwedetectdesignflawsearly?
– Manually,i.e.,pencilandpaperproofs,reflection,inspection,etc. – Automatically(=better)
The University of Sydney
Page 3
Example: UML Diagrams
– UML Diagrams
– structural/behavioral/interaction
– Example of Structural UML :
1 1..*
– Class Diagram sets in relation two sets
– Team & Employee
– Has a multiplicity constraint (composition)
– Verify by manually inspection the relationship:
– Can there be a team with no employees?
– Can an employee be in two teams?
– Can there be an employee without a team?
– Check whether this model fits its purpose? The University of Sydney
Team
Employee
Page 4
Formal Specification Languages
– Not all application semantics is expressible in UML diagrams
– Limited expressiveness – Example
• A team member must be older than 18 years, and requires an academic degree
• Not expressible in UML
– Formal Design Specification Languages – Specify design formally
– Specify constraints formally
– Express requirements formally
– Check whether design meets requirements
– Formal means requirements are defined using formal syntax and semantics Adapted from
The University of Sydney Page 5
Formal Specification Languages
– OCL (from 1997; OMG 2012)
– Textual language expressing constraints for a design
– Alloy (Jackson 2002)
– Textual language for design that can be formally checked up to a certain problem size
– Z (Spivey 1992)
– B (Abrial 2009)
– VDM – Vienna Development Method (Björner and Jones 1978) The University of Sydney
Page 6
Design by Contract (DbC)
– A software design approach for program correctness
– Known as contract programing, programming by contract,
design-by-contract programming
– Definition of formal, precise and verifiable interface specification for software components
– Pre-conditions, postconditions and invariants (contract) The University of Sydney
Page 7
Design by Contract (DbC)
By Fabuio [CC0], from Wikimedia Commons, https://commons.wikimedia.org/wiki/File:Design_by_contract.svg
The University of Sydney Page 8
Execution of Contracts
– Where can contracts/requirements be checked?
– At design time:
– Contracts/requirements are checked formally
– Formal verification tools for running these checks
– E.g., Alloy expresses design/constraints/requirements formally
– At runtime:
– Pre/Post conditions and invariants are lowered to code-level in form
of assertions.
– Requirements are checked at runtime via testing (weak approach)
The University of Sydney
Page 9
Object Constraint Language (OCL)
The University of Sydney Page 10
Object Constraint Language (OCL)
– UML diagrams not expressive enough
– Formal language for expressing constraints in SW designs
– Part of the UML standard
– Declarative
– Nosideeffects
– Nocontrolflow
The University of Sydney
Page 11
Example – Tournament Class
Tournament
– maxNumPlayers: int
+ getMaxNumPlayers():int
+ getPlayers(): List
+ acceptPlayer(p:Player)
+ removePlayer(p:Player)
+ isPlayerAccepted(p:Player):boolean
The University of Sydney Page 12
OCL Simple Predicates
“The maximum number of players in any tournament should be a positive number.”
context Tournament inv:self.getMaxNumPlayers() > 0
Notes:
– OCLusesthesamedotnotationasJava
The University of Sydney
Page 13
OCL Preconditions – Examples
“The acceptPlayer(p) operation can only be invoked if player p has not yet been accepted in the tournament.”
context Tournament::acceptPlayer(p) pre: not self.isPlayerAccepted(p)
Questions:
– Whatisthecontextthepre-condtion? – Whatis“isPlayerAccepted(p)”?
The University of Sydney
Page 14
OCL Postconditions – Example
“The number of accepted player in a tournament increases by one after the completion of acceptPlayer()”
context Tournament::acceptPlayer(p) post: self.getNumPlayers() =
self@pre.getNumPlayers() + 1
Notes:
– self@pre:thestateofthetournamentbeforetheinvocationoftheoperation – self:denotesthestateofthetournamentafterthecompletionoftheoperation
The University of Sydney Page 15
OCL Contract for acceptPlayer() in Tournament
context Tournament::acceptPlayer(p) pre: not self.isPlayerAccepted(p)
context Tournament::acceptPlayer(p) pre: self.getNumPlayers() < self.getMaxNumPlayers()
context Tournament::acceptPlayer(p) post: self.isPlayerAccepted(p)
context Tournament::acceptPlayer(p) post: self.getNumPlayers() = self@pre.getNumPlayers() + 1
The University of Sydney
Page 16
OCL Contract for removePlayer() in Tournament
context Tournament::removePlayer(p) pre: self.isPlayerAccepted(p)
context Tournament::removePlayer(p) post: not self.isPlayerAccepted(p)
context Tournament::removePlayer(p) post: self.getNumPlayers() = self@pre.getNumPlayers() - 1
The University of Sydney
Page 17
Java Implementation of Tournament class (Contract as a set of JavaDoc comments)
public class Tournament {
/** The maximum number of players
* is positive at all times.
* @invariant maxNumPlayers > 0 */
private int maxNumPlayers;
/** The players List contains
* references to Players who are * are registered with the
* Tournament. */
private List players;
/** Returns the current number of * players in the tournament. */
public int getNumPlayers() {…}
/** Returns the maximum number of * players in the tournament. */ public int getMaxNumPlayers() {…}
The University of Sydney
/** The acceptPlayer() operation * assumes that the specified
* player has not been accepted * in the Tournament yet.
* @pre !isPlayerAccepted(p)
* @pre getNumPlayers()
*
League
+start:Date +end:Date
end – start < 7
+getActivePlayers()
+start:Date +end:Date
Tournament
+acceptPlayer(p:Player)
The University of Sydney
Page 25
players
*
{ordered}
* tournaments
* tournaments * players
Player
+name:String +email:String
OCL Quantifiers
forAll
– forAll (variable|expression) is True if expression is True for all elements in the collection
exist
– exists (variable|expression) is True if there exists at least one element in the collection for which expression is True
The University of Sydney Page 26
Example: OCL Quantifiers Example
– Each Tournament conducts at least one Match on the first day of the Tournament context Tournament inv:
matches->exists(m:Match | m.start.equals(start))
– All Matches in a Tournament occur within the Tournament’s time frame
context Tournament inv: matches->forAll(m:Match |
The University of Sydney
Page 27
m.start.after(t.start) and m.end.before(t.end))
OCL Summary
– OCL is a design language – Part of UML
– Declarative
– Growing community
– OCL cannot be executed directly – Formalize your constraints / contracts
– Howtouseit?
– Translate OCL to assertions in your code
– Limited number of OCL tools for checking design/code translation/etc.
The University of Sydney Page 28
Alloy
The University of Sydney Page 29
Alloy
– ModellingLanguageforDesign,Constraints,andRequirements – Toolthatchecksthecorrectnessuptoacertainproblemsize
– Assumption:smallproblemsizesrevealmostcornercases
– Relationallogic
– Alloyusesthesamelogicfordescribingdesigns,constraints,and requirements
– for-allandexists-somequantifiersoffirst-orderlogic – operatorsofsettheoryandrelationalcalculus.
– Modellingsoftwaredesignswithsetsandrelations – Restrictions:
– onlyfirst-orderstructures,nosetsofsets,norelationsoversets. The University of Sydney
Page 30
Alloy’s Verification Process
– Process
– Expressthestructuralcomponentsandtheconstraintsoncomponents.
– AlloyAnalyzertellsifconstraintsaresatisfiedand,ifso,whatinstances satisfy the constraints.
Model (Design, Constraints, Requirements)
The University of Sydney
Page 31
Alloy Analyzer
Alloy’s Model Language
– Componentsaremodelledassets
– Basicsetoperations
– union ( + ), difference ( – ), intersection ( & ), join ( . ), etc.
– Expresscomponentstructurecoarse-grained(=unconstrained)
– Refinecomponentswithconstraintstocheckwhetherthedesignis working
The University of Sydney
Page 32
Signatures
– Introduce a set of objects and some fields
– Fields relate to other objects
– Signatures can be seen as components/object classes
– Format
sig
– Fields has the format
The University of Sydney
Page 33
Example: Signature
From Communications of the ACM, September 2019, Vol. 62 No. 9, Pages 66-76
The University of Sydney Page 34
Example (cont’d)
– Server represents the set of server nodes, and has a field causes
– If no multiplier is specified, we assume a 1:1 relationship
– Example: HTTP event has exactly one from endpoint, one to endpoint,
and one origin endpoint
– The lone multiplier specifies at most one
– The set multiplier specifies multiple elements
The University of Sydney Page 35
Constraints
– Facts
– Things that must hold
– Format:fact
– Predicates
– Defines re-usable predicates (like functions)
– Format:pred
The University of Sydney
Page 36
Example: Constraints
The University of Sydney
Page 37
–
Direction fact: every request is from, and every response is to, a client; every request is to, and every response is from, a server
Requirements
– Define a design property to check
– Checks only up to set size of 5 (grows exponentially!)
The University of Sydney Page 38
Summary
– Alloy is a modelling language
– Expresses Design, Constraints, and Requirements
– Checks the design fully automatically up to a certain set size – Verifies your design (not your program!!)
– Small problem sizes will already reveal corner cases
– Is open-source and can be downloaded from here:
– https://github.com/AlloyTools/org.alloytools.alloy – More information:
– https://cacm.acm.org/magazines/2019/9/238969-alloy/fulltext The University of Sydney
Page 39
Red, Green, Refactor
The University of Sydney Page 40
Test-Driven Development
– Test-Driven Development (TDD)
– Write test cases first before design and development – Design is evolved via refactoring
– Design → Test → Code vs. Design → Code → Test
– Tests drive the implementation
– Keep units small
– Reduce debugging effort – Self-documenting tests
The University of Sydney
Page 41
Test-Driven Development
– Red – think about what you want to develop
– Write a test that doesn’t work; doesn’t even compile at first
– Green – think about how to make your tests pass – Make test work; take short-cuts to make it work
– Refactor – think about how to improve your existing implementation
– Eliminate all short-cuts & duplication to make the test work The University of Sydney
Page 42
Red, Green, Refactor
– Red Phase
– Starting point
– Find tests for implementation
– Minimal implementation – Green
– Find solution that passes tests
– Refactor
– Improve code/ more
efficient The University of Sydney
Page 43
W12 Tutorial: Practical Exercises
Design Pattern Assignment Demo
W12 Lecture: Specification Languages
The University of Sydney
Page 44
Specifying the Model Constraints: Using asSet
League
+start:Date +end:Date
+getActivePlayers()
Local attribute navigation
context Tournament inv:
end – start <= Calendar.WEEK
Directly related class navigation
context Tournament::acceptPlayer(p) pre:
*
Tournament
+start:Date +end:Date
league.players->includes(p)
Indirectly related class navigation
{ordered}
* tournaments
+acceptPlayer(p:Player)
context League::getActivePlayers post:
players
*
* tournaments * players
Player
+name:String +email:String
The University of Sydney
Page 66
result=tournaments.players->asSet
References
– Ian Sommerville. 2016. Software Engineering (10th ed.) Global Edition. Pearson.
– Wikipedia, Software Verification and Validation, https://en.wikipedia.org/wiki/Software_verification_and_validation
– Object-Oriented Software Engineering: Using UML, Patterns, and Java, 3rd Edition, Bernd Bruegge & Allen H. Dutoit, Pearson.
The University of Sydney Page 67
References
– Craig Larman. 2004. Applying UML and Patterns: An Introduction to Object- Oriented Analysis and Design and Iterative Development (3rd Edition). Prentice Hall PTR, Upper Saddle River, NJ, USA.
– Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides.
1995. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA.
– Martin Folwer, Patterns In Enterprise Software, [https://martinfowler.com/articles/enterprisePatterns.html]
The University of Sydney
Page 68