lepus3-tutorial
21 Pages
English
Downloading requires you to have access to the YouScribe library
Learn all about the services we offer
Downloading requires you to have access to the YouScribe library
Learn all about the services we offer
21 Pages
English

Description

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

Subjects

Informations

Published by
Reads 58
Language English

Exrait

Lecture notes i nrgdaauetm dolu Ce,39E8So: waftD ergisena nrA dectuchitAuture, re mnmt 9/rD0280 Honmn A, enEd. o loohcStupmoC feca dnE reS icnec EnginelectronievintisrnireU ,g1exofy ss E
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 notation—cluttered 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 
etm daau nrgsei  nottureLec,eC dolu :oS8E93re Dftwan anesigtihcrA d ,erutce tmntuAu0820m er9/rDA nmnoH  .dEen, School of CotupmS reneica ec EndctleniroEnc niveg, Ueringinexe3E ss yfosrti
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
nce and ter ScieciE gnnilEcertno EH.n,deAmr n noC foupmohcS  loosierivUn, ngriee4xessE fo yteLtcru eonet sin graduate moduettccrihA turu,etermumn 8/9D 20038EC ,elwtfoS :9siDee ar And agn
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 )
CE, leduof S9:83eD erawtdna ngishite Arce, Actur nettumu00/8mr2 Lecture note snig arudta eomrevinU ,gnireenix5seEsf  otysi.H nedE  rD9onmAofl om C Sn,oocheicn enaupet rcSonic Engd Electr
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