CS计算机代考程序代写 Java Software Design and Construction 2 SOFT3202 / COMP9202 Design Verification & Test Driven Development

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()includes(p)
*
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 extends {
… }
– 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