lepus3-tutorial
21
pages
English
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
21
pages
English
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
ardorwLecture notes in graduate module, CE839: Software Design and Architecture, Autumn term 2008/9LePUS3 and Class-Z: desiderataLecture notes in graduate module, CE839: Software Design and Architecture, Autumn term 2008/9Dr Amnon H Eden, School of Computer Science and Electronic Engineering, University of Essex Abstraction Abstract ontology Offer an answer: What are the conceptual building blocks of software design? Scaling: capture the building blocks of very large programsObject-Oriented Modelling Detailed notation—cluttered diagrams What NOT to model? What a specification should NOT represent? Rigourin LePUS3 and Class-Z Formal specification Verification Decidability: Tool support in “round-trip engineering” automated verification is possible in principle Tool support automates the verification process Allows us to “close the loop” of round-trip engineering Visualization (OptionalModelling small programs Offer a “picture” of a specification: Existing program: a ‘roadmap’ to the millions of lines of codeModelling large programs A design motif: design pattern, architectural style Makes software easier to understand and changeModelling application frameworks Theory & practice Be relevant to practical applicationsModelling design patterns Provide a sound foundation in a solid mathematical theory1 2What can be modelled in LePUS3/Class-Z?Specification language: desiderata(cont.) Programs Design patterns Combine ...
Voir
Publié par
Langue
English
lication frameworks http A (Collections in java.util) Servl (The Iterator pattern) servlet Ops
4
Specification language: desiderata (cont.) Combine theory & practice It has long been my personal view that the separation of practical and theoretical work is artificial and injurious. Much of the practical work done in computing, both in software and in hardware design, is unsound and clumsy because the people who do it have not any clear understanding of the fundamental design principles of their work. Most of the abstract mathematical and theoretical work is sterile because it has no point of contact with real computing. -- Christopher Strachey
3
2
Lecture notes in graduate module, CE839: Software Desi gn and Architecture, Autumn term 2008/9 Dr Amnon H Eden, School of Computer Science and Electro nic Engineering, University of Essex Object-Oriented Modelling in LePUS3 and Class-Z
LePUS3 and Class-Z : desiderata Abstraction Abstract ontology Offer an answer: What are the conceptual building blocks of software design? Scaling: capture the building blocks of very large progra ms Detailed notationcluttered diagrams What NOT to model? What a specification should NOT repr esent? Rigour Formal specification Verification Decidability: Tool support in “round-trip engineering automated verification is possible in principle Tool support automates the verification process Allows us to “close the loop of round-trip engineering Visualization (Optional Offer a “picture of a specification: Existing program: a ‘roadmap’ to the millions of lines of code A design motif: design pattern, architectural style Makes software easier to understand and change Theory & practice Be relevant to practical applications Provide a sound foundation in a solid mathematical the ory
1
Modelling small programs Modelling large programs Modelling application frameworks Modelling design patterns
servlet Ops user Servlet (Java Servlets)
What can be modelled in LePUS3 / Class-Z ? Pro rams Desi n atterns
8
The genealogy of LePUS3 and Class-Z Definition: As a subset of first-order predicate calculus (classical logic) Official reference manual: A.H. Eden, E. Gasparis, J. Nicholson. " LePUS3 and Class-Z Reference Manual ". University of Essex, Tech. Rep. CSM-474, ISSN 1744-8050 (2007). htt ://le us.or .uk/ref/refman/refman.xml Historical roots: LePUS3 : LePUS [Eden 2001]LanguagE for Pattern Uniform Specification Class-Z : Z [Spivey]
What cannot be modelled in LePUS3 / Class-Z ? Temporal relations ‘Method x should be called before method y’ No collaboration/interaction diagrams, flow charts, statecharts,
Statements about specific objects Strategic design Architectural styles Components Programs in procediural/functional/other programming parad gms LePUS3 and Class-Z model object-oriented programs
5
7
LePUS3 vs. Class-Z Specifications can be expressed in one of two ways: LePUS3 : Visual, similar to UML Class Diagrams Class-Z : symbolic, similar to Z Students are only required to learn one of the notations ava.lang. LePUS3 jSystem Member printStream Example java.lang . system , printStream : CLASS Class-Z Member ( java.lang.system,printStream )
Forward engineering Reverse engineering (Verification) (Design Recovery) interface Collection ... { public Iterator iterator() { lication ... App s blic cla }pupublic Itsesr aLtionkre diLtiesrtat.o.r.( ){ { AClpaps.s flriabmaeriwesorks r ... } } Implementation
Formal specification Software modelling Software visualization
Tool support in LePUS3 and Class-
eL gins tenoe urctel ,omudta earudare oftw9: SCE83es2x fsEE .H nonhcS ,ned00 2rmteAmr 9D8/ru,eettcmu nA tugn aDesirchind A ,gnvinUisreo ytontr EicinngrieecSeicn ena dlEceool of Computer 
Modelling individual classes class constant : represents any specific static type such as a class, Java interface, and primitive types
Modelling properties Unary relation : represents a property Class AbstractSet is abstract Collection is an Interface Collection.newItr is Example an abstract method abstractSet , collection : CLASS newItr : SIGNATURE Abstract ( abstractSet ) Abstract ( collection ) Abstract ( newItr ⊗ collection )
Modelling individual methods signature constant : represents a specific ‘signature’ of (one or more) methods A method with signature newItr is defined in class Collection linkedList collection newItr newItr
A method with signature newItr is defined in class LinkedList public class LinkedList ... { public Iterator newItr() { ... Example } } linkedList , collection : CLASS public class Collection ... { newItr : SIGNATURE public Iterator newItr() { Method ( newItr ⊗ linkedList ) } ... Method ( newItr ⊗ collection ) }
Modelling small programs in LePUS3 and Class-Z
Class and signature constants Unary relation symbols Binary relation symbols
9
class interface primitive type LinkedList Collection int Example linkedList , collection , int : CLASS
10
Binary relations: Call Note that the Call relation abstracts away all p u bl i c c lass Test { p u b l ic s t ati c voi d main(String[] args) { information about the i f (args.length == 0) control-flow System.out.print("Insufficient arguments"); ...
Modelling relations between individuals Binary relation : represents a relation between two individuals ListIter In ListIterator linkedList Inherit abstractSet herit LinkedList ‘extends’ ListIter ‘implements’ AbstractSet ListIterator Example linkedList , abstractSet , ListItr , ListIterator : CLASS Inherit ( linkedList , abstractSet ) Inherit ( ListItr , ListIterator )
jaSvyas.tleanmg. Member printStream Example java.lang . system , printStream : CLASS Member ( java.lang.system,printStream )
Binary relations: Member public clas s System { ... public stati c PrintStream out; ... }
Binary relations: Aggregate
Example linkedList , object : CLASS Aggregate ( linkedList,object )
15
test printStream main Call print Example test , printStream : CLASS ma , print : SIGNATURE in Call ( main ⊗ test , print ⊗ printStream )
Modelling indirect relations Transitive relation : represents possibly indirect relation (the ‘transitive closure’ of a binary relation) interface Collection { ... class AbstractList i m p l emen ts Collection {... class AbstractSet e x t e n ds AbstractList ... class LinkedList e x t e n d s AbstractSet ... linkedList Inherit + collection Example linkedList , collection : CLASS Inherit + ( linkedList , collection )
Binary relations: Produce p u b l i c c l as s LinkedList { ... p u bl i c ListIterator listIterator( in t index) { if (1 < 0) r et urn n e w ListItr(index); } ... } linkedList Produce : listIterator P oduce listItr A special kind of a Create r relation in which the new object is returned Method LinkedList.listIterator may (typical to ‘factory methods’) create and return a new ListItr Example linkedList , listItr : CLASS listIterator : SIGNATURE Produce ( listIterator ⊗ linkedList , listItr )
Binary relations: Create
public class MyClass { public void method() { ... i f ... e l s e ... ... fo r ( i n t index = 0; ...) ... }... }
Method MyClass.method may create an integer Example linkedList , listItr : CLASS listIterator : SIGNATURE Produce ( listIterator ⊗ linkedList , listItr )
Binary relations: Forward
p u b l i c c l as s MyServlet ex t en d s HttpServlet { p u bl i c v o i d doGet(HttpServletRequest rq, HttpServletResponse rs ) { s u pe r .doGet(rq,rs); } Forward : myServlet httpServlet A a Call d et re lsaptieocni ailn kiwnhdi cohf the doGet Forward oG formal arguments are passed on to a method with same signature Method MyServlet.doGet forwards the call to HttpServlet.doGet Example myServlet , httpServlet : CLASS doGet : SIGNATURE Forward ( doGet ⊗ myServlet , doGet ⊗ httpServlet )
24
ioException fileInput Str ioException read nullPointer Exception nu o nter Exception Example fileInputStream , ioException , nullPointerException : CLASS read,nullPointerException,ioException : SIGNATURE Call + ( read ⊗ fileInputStream , ioException ⊗ ioException ) Call + ( read ⊗ fileInputStream , nullPointerException ⊗ nullPointerException )
Case Study II: java.io.XXReader classes p u b l i c c l as s LineNumberReader e x te n d s BufferedReader { … p u bl i c v o id read() { … s u pe r .read(); … } … p u bl i c v o id mark( in t readAheadLimit) { … s u pe r .mark(readAheadLimit); … } … p u bl i c v o id reset() { … s u pe r .reset(); … } … ReaderExample bufferedReader , lineNumberReader : CLASS read , mark, reset : SIGNATURE Forward ( read ⊗ lineNumberReader , read ⊗ bufferedReader ) Forward (mark ⊗ lineNumberReader , mark ⊗ bufferedReader ) Forward (reset ⊗ lineNumberReader , reset ⊗ bufferedReader )
Exercise “Translate the L ePUS3 chart in the case study into a Class-Z specification Use either Class-Z or LePUS to model three DIFFERENT specifications of the classes Collection , Iterator , LinkedList , and ListItr in the package java.util . Each specification should include one or more of the methods defined in these classes. Which ones did you choose to model and why? Note that each specification may contain a different set of relations Note that each specification must be SATISFIED by the classes in java.util !
LinkedList ListItr newItr() next() return new ListItr(); Object
Case Study I: LinkedList and ListItr LePUS3 UML Class diagram Collection Iterator newItr() next()
Transitive relations II p u b l i c c l as s FileInputStream ... { p u bl i c i n t read(byte[] b) t h ro w s IOException, NullPointerException { ...
22
m etludorg naudaSo: waft Ce,39E8 notes iLecturefo yssE 6xe ,erutuAtihcutceann Ard Dreiges .dEne ,A nmnoH 2008/9Drmn term E dna ecneicS reutmpCof oolhoScsrtiinev,gU reniginec Enronilect
