lepus3-tutorial

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

Informations

• Publié par: Nopod
• Nombre de lectures: 58
• Langue: English

Extrait

Lecture notes i nrgdaauetm dolu Ce,39E8So: waftD ergisena nrA dectuchitAuture, re mnmt 9/ rD 0280  Honmn A, enEd. o loohcStupmoC feca dnE reS icnec EnginelectronievintisrnireU ,g 1 exofy 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 proced i ural/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 j System 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 } pu public It s e s r   a L t i o nk r e   d i L t i e s r t at . o . r . (   ) {  { A Cl p a p s . s     f l r i a b m a e ri w es orks r ... } } Implementation

Formal specification Software modelling Software visualization

Tool support in LePUS3 and Class-

eL gins tenoe urctel ,omudta earudare oftw9: SCE83 es 2 x fsEE .H nonhcS ,ned 00 2rmte Amr  9 D 8/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, Ueringinexe 3 E 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, ngriee 4 xessE fo yt eLtcru eonet sin graduate moduettccrihA turu,etermumn 8/9 D  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 )

ja S v y a s . t l e an m g. 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 eom revinU ,gnireenix 5 seEsf  otysi.H nedE  rD 9 onmAofl 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   l s a p ti e o c n i   a i l n     ki w n h d i   c o h f  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 iLecture fo yssE  6 xe  ,erutuAtihcutceann Ard  Dreiges  .dEne ,A nmnoH  2008/9 Dr mn term  E dna ecneicS reutmpCof  oolhoScsrtiinev,gU reniginec Enronilect