[SOLVED] 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

Copyright Warning

COMMONWEALTH OF AUSTRALIA

Copyright Regulations 1969

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 copyrightprotection 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 users 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

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 stakeholders 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

ModelingOO-Contracts Formal Specifcation

Natural Language

Mathematical Notation

Models and contracts:
Alanguage 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)

< >
!containsKey(key)

< >
get(key) == entry

The University of Sydney Page 28

Use Contracts inRequirements 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() =

[email protected]() + 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() + 1The University of Sydney Page 38OCL Contract for removePlayer()in Tournamentcontext Tournament::removePlayer(p) pre:isPlayerAccepted(p)context Tournament::removePlayer(p) post:not isPlayerAccepted(p)context Tournament::removePlayer(p) post:getNumPlayers() = @pre.getNumPlayers() – 1The University of Sydney Page 39Java Implementation ofTournament 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 isin 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)
Intersectionwith 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 theCollection 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.WEEKDirectly related class navigationcontext 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