程序代写代做代考 Java Software Construction & Design 1

Software Construction & Design 1

The University of Sydney Page 1

Software Design and

Construction 2

SOFT3202 / COMP9202

Software Verification

Theory and Examples

School of Information Technologies

Dr. Basem Suleiman

The University of Sydney Page 2

COMMONWEALTH OF AUSTRALIA

WARNING

This material has been reproduced and communicated to
you by or on behalf of the University of Sydney
pursuant to Part VB of the Copyright Act 1968 (the
Act ).

The material in this communication may be subject
to copyright under the Act. Any further copying or
communication of this material by you may be the
subject of copyright protection under
the Act.

Do not remove this notice.

The University of Sydney Page 3

Agenda

– Software Verification Theory

– Design by Contract
– Pre-conditions and post-conditions

– Class invariants

The University of Sydney Page 4

Software Validation and

Verification

Theory

The University of Sydney Page 5

Software Testing – Revisit

– Software process to
– Demonstrate that software meets its requirements (validation testing)

– Find incorrect or undesired behavior caused by defects/bugs (defect testing)
• E.g., System crashes, incorrect computations, unnecessary interactions and data

corruptions

– Part of software verification and validation (V&V) process

The University of Sydney Page 6

Software Verification and Validation

– Software testing is part of software Verification and Validation (V&V)

– The goal of V&V is to establish confidence that the software is “fit for purpose”

– Software Validation
– Are we building the right product?

– Ensures that the software meets customer expectations/needs

– Software Verification
– Are we building the product right?

– Ensures that the software meets its stated functional and non-functional

requirements

The University of Sydney Page 7

Software V&V

– Software Verification
– Concerned with the software requirements/specifications

– Can be ambiguous

– Software Validation
– Customer/end user’s expectation

– Disambiguate the requirements

The University of Sydney Page 8

V-Model

– Link each phase of the SDLC with its associated testing phase

– Each verification stage relates to a validation stage

https://www.buzzle.com/editorials/4-5-2005-68117.asp

The University of Sydney Page 9

Software Verification

– Artifact/specification verification
– Review the resulted software artifacts to verify that specifications are met

– Check the output of each software development phase against the input

specification (specs.)

– Design specifications against requirement specifications
• Detailed design correctly implement the requirements (F & NF)

– Construction (code) against the design specs.
• Source code/user interfaces correctly implements the design specs.

– Include inspections, reviews, walkthrough

The University of Sydney Page 10

Static Verification

– Static Verification

– Static system analysis to discover problems

– May be applied to requirements, design/models, configuration and test data

– Reviews

– Walk through

– Code inspection

The University of Sydney Page 11

Software Validation

– Artifact/specification validation
– Validate the requirements from the end user perspective

– Check that the needs of all stakeholders (users, managers, investors) are met
– Validate the output of main development stages from the stakeholder’s point of

view

• Validate if the requirements represent the will and goals of the

stakeholders

– Include Unit testing, integration/functional testing, and user acceptance

testing

The University of Sydney Page 14

Design by Contract

The University of Sydney Page 15

Contract

– A lawful agreement between two parties in which both
parties accept obligations and on which both parties can
found their rights

– The remedy for breach of a contract is usually an award of
money to the injured party

The University of Sydney Page 16

Object-Oriented Contract

– Specifies the expected services that can be provided if
certain conditions are satisfied

– Services = “Obligations” and conditions = “Rights”

– Breach of a contract results in generating an exception

The University of Sydney Page 17

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 18

Design by Contract (DbC)

By Fabuio [CC0], from Wikimedia Commons, https://commons.wikimedia.org/wiki/File:Design_by_contract.svg

https://commons.wikimedia.org/wiki/File:Design_by_contract.svg

The University of Sydney Page 19

Contracts in OO Design

Object-oriented contract

– Describes the services that are provided by an object if
certain conditions are fulfilled

– services = “obligations”, conditions = “rights”

– An OO-contract for each service specifically describes:
– The conditions under which the service will be provided

– A specification of the result of the service that is provided

– The remedy for breach of an OO-contract is the generation
of an exception

The University of Sydney Page 20

Object-Oriented Contract –

– Examples:
– A letter posted before 18:00 will be delivered on the next working day

to any address within Australia

– For the price of $7 a letter with a maximum weight of 80 grams will be
delivered anywhere in Australia within 4 hours of pickup

– Exercise: identify the conditions/rights and obligations/services of the
above delivery services.

The University of Sydney Page 21

Modeling Constraints

with Contracts

The University of Sydney Page 23

Modeling Constraints with Contracts

– Example of constraints in Arena:
– An already registered player cannot be registered again

– The number of players in a tournament should not be more than
maxNumPlayers

– One can only remove players that have been registered

– We model them with contracts

– Contracts can be written in OCL

The University of Sydney Page 24

Modeling OO-Contracts – Formal Specifcation

– Natural Language

– Mathematical Notation

– Models and contracts:
– A language for the formulation of constraints with the formal strength

of the mathematical notation and the easiness of natural language:

 UML + OCL (Object Constraint Language)

– Uses the abstractions of the UML model

– OCL is based on predicate calculus

The University of Sydney Page 25

Contracts and Formal Specification

– A Contract share same assumptions about the class

– Three constraints:
– Invariant:

• A predicate that is always true for all instances of a class

– Precondition (“rights”):

• Must be true before an operation is invoked

– Postcondition (“obligation”):

• Must be true after an operation is invoked.

The University of Sydney Page 26

Formal Specification

– A contract is called a formal specification, if the invariants,
rights and obligations in the contract are unambiguous

The University of Sydney Page 27

Expressing Constraints in UML Models

HashTable

put(key,entry:Object)
get(key):Object
remove(key:Object)
containsKey(key:Object):boolean
size():int

numElements:int

<>
numElements >= 0<>

!containsKey(key)

<>
containsKey(key)

<>
!containsKey(key)

<>
get(key) == entry

The University of Sydney Page 28

Use Contracts in Requirements Analysis

– Many constraints represent domain-level information

– Why not use them in requirements analysis?

– Increase requirements precision

– Yield more questions for the end user

– Clarify the relationships among several objects

– Constraints are sometimes used during requirements
analysis, however there are trade-offs

The University of Sydney Page 30

Object Constraint

Language (OCL)

The University of Sydney Page 31

Object Constraint Language (OCL)

– Formal language for expressing constraints over a set of objects and their
attributes

– Part of the UML standard

– Used to write constraints that cannot otherwise be expressed in a diagram

– Declarative

– No side effects

– No control flow

– Based on Sets and Multi Sets

The University of Sydney Page 32

OCL Basic Concepts

– OCL expressions

– Return True or False

– Are evaluated in a specified context

– All constraints apply to all instances

The University of Sydney Page 33

Example – Tournament Class

Tournament

– maxNumPlayers: int

+ acceptPlayer(p:Player)

+ removePlayer(p:Player)

+ getMaxNumPlayers():int

+ getPlayers(): List

+ isPlayerAccepted(p:Player):boolean

The University of Sydney Page 34

OCL Simple Predicates

“The maximum number of players in any tournament should be a
positive number.”

context Tournament inv: self.getMaxNumPlayers() > 0

Notes:

– OCL uses the same dot notation as Java

The University of Sydney Page 35

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:

– What is the context the pre-condtion?

– What is “isPlayerAccepted(p)”?

The University of Sydney Page 36

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: the state of the tournament before the invocation of the operation

– self: denotes the state of the tournament after the completion of the operation

The University of Sydney Page 37

OCL Contract for acceptPlayer() in Tournament

context Tournament::acceptPlayer(p) pre:

not isPlayerAccepted(p)

context Tournament::acceptPlayer(p) pre:

getNumPlayers() < getMaxNumPlayers() context Tournament::acceptPlayer(p) post: isPlayerAccepted(p) context Tournament::acceptPlayer(p) post: getNumPlayers() = @pre.getNumPlayers() + 1 The University of Sydney Page 38 OCL Contract for removePlayer() in Tournament context Tournament::removePlayer(p) pre: isPlayerAccepted(p) context Tournament::removePlayer(p) post: not isPlayerAccepted(p) context Tournament::removePlayer(p) post: getNumPlayers() = @pre.getNumPlayers() - 1 The University of Sydney Page 39 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 acceptPlayer() operation

* assumes that the specified

* player has not been accepted

* in the Tournament yet.

* @pre !isPlayerAccepted(p)

* @pre getNumPlayers()includes(p)

The University of Sydney Page 47

OCL Sets, Bags and Sequences

– Sets, Bags and Sequences are predefined in OCL
– Subtypes of Collection

– OCL offers a large number of predefined operations on
collections. All of the form:

collection->operation(arguments)

The University of Sydney Page 48

OCL-Collection

– The OCL-Type Collection is the generic superclass of a collection of objects
of Type T

– Subclasses of Collection are

– Set: Set in the mathematical sense. Every element can appear only once

– Bag: A collection, in which elements can appear more than once (also called
multiset)

– Sequence: A multiset, in which the elements are ordered

– Example for Collections:

– Set(Integer): a set of integer numbers

– Bag(Person): a multiset of persons

– Sequence(Customer): a sequence of customers

The University of Sydney Page 49

OCL-Operations for OCL-Collections (1)

size: Integer

Number of elements in the collection

includes(o:OclAny): Boolean

True, if the element o is in the collection

count(o:OclAny): Integer

Counts how many times an element is contained in the collection

isEmpty: Boolean

True, if the collection is empty

notEmpty: Boolean

True, if the collection is not empty

The OCL-Type OclAny is the most general OCL-Type

The University of Sydney Page 50

OCL-Operations for OCL-Collections(2)

union(c1:Collection)
Union with collection c1

intersection(c2:Collection)
Intersection with Collection c2 (contains only elements, which appear in the collection as
well as in collection c2 auftreten)

including(o:OclAny)
Collection containing all elements of the Collection and element o

select(expr:OclExpression)
Subset of all elements of the collection, for which the OCL-expression expr is true

The University of Sydney Page 51

Evaluating OCL Expressions
The value of an OCL expression is an object or a collection of objects.

– Multiplicity of the association-end is 1

– The value of the OCL expression is a single object

– Multiplicity is 0..1

– The result is an empty set if there is no object, otherwise a single object

– Multiplicity of the association-end is *

– The result is a collection of objects

• By default, the navigation result is a Set

• When the association is {ordered}, the navigation results in a
Sequence

• Multiple “1-Many” associations result in a Bag

The University of Sydney Page 52

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 53

OCL Quantifiers – forAll Example

Given the following OCL quantifier

context Tournament inv:

matches->forAll(m:Match |

m.start.after(t.start) and m.end.before(t.end))

Exercise: explain what this OCL attempts to verify.

The University of Sydney Page 55

OCL Quantifiers – Exists Example

Given the following OCL quantifier

context Tournament inv:

matches->exists(m:Match | m.start.equals(start))

The University of Sydney Page 59

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.

http://vig.prenhall.com/catalog/academic/product/0,4096,0130471100,00.html

The University of Sydney Page 60

W12 Tutorial: Practical

Exercises

Design Pattern Assignment

Demo

W12 Lecture: Specification

Languages

The University of Sydney Page 69

Specifying the Model Constraints: Using asSet

Local attribute navigation

context Tournament inv:

end – start <= Calendar.WEEK Directly related class navigation context Tournament::acceptPlayer(p) pre: league.players->includes(p)

players

* tournaments

{ordered}

Tournament

+start:Date

+end:Date

+acceptPlayer(p:Player)

League

+start:Date

+end:Date

+getActivePlayers()

Player

+name:String

+email:String

* players

tournaments*

Indirectly related class navigation
context League::getActivePlayers

post:

result=tournaments.players->asSet

Published by admin

Leave a Reply Cancel reply