Specification Ch. 5 1 Outline • Discussion of the term "specification" • Types of specifications – operational • • • • Data Flow Diagrams (Some) UML diagrams Finite State Machines Petri Nets – descriptive • Entity Relationship Diagrams • Logic-based notations • Algebraic notations • Languages for modular specifications – Statecharts –Z Ch. 5 2 Specification • A broad term that means definition • Used at different stages of software development for different purposes • Generally, a statement of agreement (contract) between – producer and consumer of a service – implementer and user • All desirable qualities must be specified Ch. 5 3 Uses of specification • Statement of user requirements – major failures occur because of misunderstandings between the producer and the user – "The hardest single part of building a softwarem system is deciding precisely what to build" (F. Brooks) Ch. 5 4 Uses of specification (cont.) • Statement of the interface between the machine and the controlled environment – serious undesirable effects can result due to misunderstandings between software engineers and domain experts about the phenomena affecting the control function to be implemented by software Ch. 5 5 Uses of specification (cont.) • Statement of requirements for implementation – design process is a chain of specification (i.e., definition)–implementation–verification steps • requirements specification refers to definition of external behavior – design specification must be verified against it • design specification refers to definition of the software architecture – code must be verified against it Ch. 5 6 Uses of specification (cont.) • A reference point during maintenance – corrective maintenance only changes implementation – adaptive and perfective maintenance occur because of requirements changes • requirements specification must change accordingly Ch. 5 7 Specification qualities • Precise, clear, unambiguous • Consistent • Complete – internal completeness – external completeness • Incremental Ch. 5 8 Clear, unambiguous, understandable • Example: specification fragment for a word-processor Selecting is the process of designating areas of the document that you want to work on. Most editing and formatting actions require two steps: first you select what you want to work on, such as text or graphics; then you initiate the appropriate action. can an area be scattered? Ch. 5 9 Precise, unambiguous, clear • Another example (from a real safetycritical system) The message must be triplicated. copies must be forwarded through different physical channels. The accepts the message on the basis two-out-of-three voting policy. The three three receiver of a can a message be accepted as soon as we receive 2 out of 3 identical copies of message or do we need to wait for receipt of the 3rd? Ch. 5 10 Consistent • Example: specification fragment for a word-processor The whole text should be kept in lines of equal length. The length is specified by the user. Unless the user gives an explicit hyphenation command, a carriage return should occur only at the end of a word. What if the length of a word exceeds the length of the line? Ch. 5 11 Complete • Internal completeness – the specification must define any new concept or terminology that it uses • glossary helpful for this purpose – the specification must document all the needed requirements • difficulty: when should one stop? Ch. 5 12 Incremental • Referring to the specification process – start from a sketchy document and progressively add details • Referring to the specification document – document is structured and can be understood in increments Ch. 5 13 Classification of specification styles • Informal, semi-formal, formal • Operational – Behavior specification in terms of some abstract machine • Descriptive – Behavior described in terms of properties Ch. 5 14 Example 1 • Specification of a geometric figure E: E can be drawn as follows: 1. Select two points P1 and P2 on a plane 2. Get a string of a certain length and fix its ends to P1 and P2 3. Position a pencil as shown in next figure 4. Move the pen clockwise, keeping the string tightly stretched, until you reach the point where you started drawing this is an operational specification Ch. 5 15 Ch. 5 16 A descriptive specification • Geometric figure E is describe by the following equation ax2 + by2 + c = 0 where a, b, and c are suitable constants Ch. 5 17 Another example OP “Let a be an array of n elements. The result of its sorting is an array b of n elements such that the first element of b is the minimum of a (if several elements of a have the same value, any one of them is acceptable); the second element of b is the minimum of the array of n-1 elements obtained from a by removing its minimum element; and so on until all n elements of a have been removed.” “The result of sorting array a is an array b which is a DES permutation of a and is sorted.” Ch. 5 18 How to verify a specification? • “Observe” dynamic behavior of specified system (simulation, prototyping, “testing” specs) • Analyze properties of the specified system • Analogy with traditional engineering – physical model of a bridge – mathematical model of a bridge Ch. 5 19 Data Flow Diagrams (DFDs) • A semi-formal operational specification • System viewed as collection of data manipulated by “functions” • Data can be persistent – they are stored in data repositories • Data can flow – they are represented by data flows • DFDs have a graphical notation Ch. 5 20 Graphical notation – bubbles represent functions – arcs represent data flows – open boxes represent persistent store – closed boxes represent I/O interaction The function sym bol The input device sym bol The data flow symbol The output device sym bol The data store symbol Ch. 5 21 Example b + a d c * specifies evaluation of (a + b) * (c + a * d) + * Ch. 5 22 A construction “method” (1) 1. Start from the “context” diagram Input Input O utput 1 inform ation 2 Input n ... system O utput ... O utput Ch. 5 1 2 m 23 A construction “method” (2) 2. Proceed by refinements until you reach “elementary” functions (preserve balancing) A I H I O A3 J A4 A1 A6 P K Q M A2 S A5 N A7 R K B2 K2 O M B1 K3 K1 T Ag B4 B3 N K4 Ch. 5 24 A library example Boo k Boo k requ est by th e u ser Sh elv es Title and au th or of req uested b ook; name of th e u ser Auth or Boo k List o f A uthors Get a bo ok Boo k reception Title Boo k title; user n ame List o f titles List o f b oo ks bo rrowed Title Search by topics List o f top ics Top ic Top ic List o f titles referring to the to pic Disp lay of the list of titles Top ic requ est by th e u ser Ch. 5 25 Refinement of “Get a book” Book Shelves Author Get the book Book List of Authors <shelf#, book#> Title Find book position Book reception List of books borrowed List of titles Title and author of requested book; name of the user Book title; user name Book request by the user Ch. 5 26 Patient monitoring systems The purpose is to monitor the patients’ vital factors--blood, pressure, temperature, …--reading them at specified frequencies from analog devices and storing readings in a DB. If readings fall outside the range specified for patient or device fails an alarm must be sent to a nurse. The system also provides reports. N urse R eport R equest P atient C linical D ata R eport P atient M onitoring N urse A larm R ecent data D ata for report Ch. 5 P ersistent data 27 A refinement P atient archive R ecent D ata R eport R equest D ata for R eport N urse G enerate R eport U pdate archive R eport F orm atted data C entral M onitoring L im its L im its for patient N urse A larm P atient data L ocal M onitoring Ch. 5 C linical D ata P atient 28 More refinement P atient P ressure L im its P ressure, pulse… T em perature C heck lim it violations data decode P ulse R esult F orm at data D ate T im e clock produce m essage F orm atted data alarm Ch. 5 29 An evaluation of DFDs (1) • Easy to read, but … • Informal semantics – How to define leaf functions? – Inherent ambiguities A E B • Outputs from A, B, C are all needed? • Outputs for E and F are produced at the same time? D F C Ch. 5 30 An evaluation of DFDs (2) • Control information is absent A B Possible interpretations: (a) A produces datum, waits until B consumes it (b) B can read the datum many times without consuming it (c) a pipe is inserted between A and B Ch. 5 31 Formalization/extensions • There have been attempts to formalize DFDs • There have been attempts to extend DFDs (e.g., for real-time systems) d1 T rigger d2 . . . dn Ch. 5 32 UML use-case diagrams • Define functions on basis of actors and actions borrow book return book librarian customer library update Ch. 5 33 UML sequence diagrams • Describe how objects interact by exchanging messages • Provide a dynamic view C usto m er L ib rarian C atalo gue m em b er card + b o o k req uest m em b ership OK b o o k req uest tim e b o o k availab le b o o k b o rro w ed Ch. 5 34 UML collaboration diagrams • Give object interactions and their order • Equivalent to sequence diagrams 2 : m em b ership O K 1 : m em b er card + b o o k req uest C ustom er 3 : b o o k req uest Librarian 5 : b o o k b o rro w ed C atalogue 4 : b o o k availab le Ch. 5 35 Finite state machines (FSMs) • Can specify control flow aspects • Defined as a finite set of states, Q; a finite set of inputs, I; a transition function d : Q x I Q (d can be a partial function) a q1 a b q0 q2 c b q3 Ch. 5 36 Example: a lamp Push switch Off On Push switch Ch. 5 37 Another example: a plant control system H ig h -p re s s u re a la rm H ig h -te m p e ra tu re a la rm On O ff R e s ta rt Ch. 5 38 A refinement Pressure signal Pressure Pressure action action Successful recovery Temperature signal Unsuccessful recovery Normal Off Normal Off Successful recovery Temperature signal Unsuccessful recovery Temperature action Ch. 5 Pressure signal 39 Classes of FSMs • Deterministic/nondeterministic • FSMs as recognizers – introduce final states • FSMs as transducers – introduce set of outputs •... Ch. 5 40 FSMs as recognizers q1 e g q2 q3 i q 4 n b q0 qf e q5 q6 n d qf is a final state Ch. 5 41 FSMs as recognizers < le tte r> < d ig it> q < le tte r> 0 q1 _ < le tte r> Legend: < le tte r> < d ig it> q2 < d ig it> is a n a b b re via tio n fo r a s e t o f a rro w s la b e le d a , b ,..., z, A ,..., Z , re s p e c tive ly is a n a b b re via tio n fo r a s e t o f a rro w s la b e le d 0 , 1 ,..., 9 , re s p e c tive ly Ch. 5 42 Limitations • Finite memory • State explosion – Given a number of FSMs with k1, k2, … kn states, their composition is a FSM with k1 * k2 *… * kn. This growth is exponential with the number of FSMs, not linear (we would like it to be k1 + k2 +… + kn ) Ch. 5 43 State explosion: an example p ro d u ce P ro d u ce r p1 p2 d e p o sit get C o n su m e r c1 c2 co n su m e d e p o sit d e p o sit S to ra g e 0 1 gCh. et 5 2 get 44 The resulting FSM w rite w rite < 1 , p ,c > 1 1 < 0 , p ,c > 1 1 consum e consum e p ro d u c e consum e p ro d u c e < 0 , p ,c > 2 1 < 2 , p ,c > 1 1 p ro d u c e < 1 , p ,c > 2 1 < 2 , p ,c > 2 1 re a d < 0 , p ,c > 1 2 < 1 , p ,c > 1 2 < 2 , p ,c > 1 2 re a d p ro d u c e consum e <0, p , c > 2 2 re a d w rite p ro d u c e consum e re a d w rite < 1 , p ,c > 2 2 Ch. 5 p ro d u c e consum e < 2 , p ,c > 2 2 45 Petri nets A quadruple (P,T,F,W) P: places T: transitions (P, T are finite) F: flow relation (F {PT} {TP} ) W: weight function (W: F N – {0} ) Properties: (1) P T = Ø (2) P T Ø (3)F (P T) (T P) (4) W: F N-{0} Default value of W is 1 State defined by marking: M: P N Ch. 5 46 Graphical representation p la ce s m a rk in g tra n sitio n s P flo w s 3 w e ig h t P 2 1 t 1 t P 3 P 2 P 5 4 t t 4 3 P P 7 6 t 5 t Ch. 5 6 47 Semantics: dynamic evolution • Transition t is enabled iff – p t's input places, M(p) W(<p,t>) • t fires: produces a new marking M’ in places that are either t's input or output places or both – if p is an input place: M'(p) = M(p) - W(<p,t>) – if p is an output place: M'(p) = M(p) + W(<t,p>) – if p is both an input and an output place: M'(p) = M(p) - W(<p,t>) + W(<t,p>) Ch. 5 48 Nondeterminism • Any of the enabled transitions may fire • Model does not specify which fires, nor when it fires Ch. 5 49 Modeling with Petri nets • Places represent distributed states • Transitions represent actions or events that may occur when system is in a certain state • They can occur as certain conditions hold on the states Ch. 5 50 after (a) either (b) or (c) may occur, and then (d) P2 P1 P P1 2 t1 t1 3 P P t4 t3 P t5 t4 t3 P P7 6 P7 6 P5 4 P5 4 t5 t6 t6 (b) (a) P P1 t 2 t P 4 P2 P1 1 P3 P t2 P t2 P3 t2 1 P P P5 4 5 t4 t3 P P 6 t4 t3 P 6 7 t5 7 t5 t6 t6 Ch. 5 (c) t2 P3 51 (d) Common cases • Concurrency – two transitions are enabled to fire in a given state, and the firing of one does nor prevent the other from firing • see t1 and t2 in case (a) • Conflict – two transitions are enabled to fire in a given state, but the firing of one prevents the other from firing • see t3 and t4 in case (d) • place P3 models a shared resource between two processes – no policy exists to resolve conflicts (known as unfair scheduling) – a process may never get a resource (starvation) Ch. 5 52 How to avoid starvation P1 P2 P3 t1 P 4 t3 t2 imposes alternation P 5 t4 P P 6 7 t t6 5 Ch. 5 53 A conflict-free net P P 1 t1 t 2 2 R t'3 t' 4 t" 3 this net can deadlock! consider ' ' t1 , t 3 , t 2, t 4 t" 4 2 2 t t 6 5 Ch. 5 54 A deadlock-free net P P 1 t1 t 2 2 R t'3 2 t' 2 4 t" 3 t" 4 t t 5 2 6 2 Ch. 5 55 A case of partial starvation t1 t t3 t Ch. 5 2 4 56 Producer-consumer example (1) write consume P 1 P 2 C 2 C1 produce read separate nets for the subsystems read 0 read 1 write Ch. 5 2 write 57 Producer-consumer example (2) consume C1 C2 read read one net for the entire system 0 1 2 write write P1 produce Ch. 5 P2 58 Limitations and extensions P channel1 channel2 Token represents a message. You wish to say that the delivery channel depends on contents. How? Petri nets cannot specifyCh.selection policies. 5 59 Extension 1 assigning values to tokens • Transitions have associated predicates and functions • Predicate refers to values of tokens in input places selected for firing • Functions define values of tokens produced in output places Ch. 5 60 Example P 2 P 1 P 7 3 1 4 4 t1 t2 P 4 P 5 3 Predicate P2 > P1 and function P4 := P2 + P1 associated with t1 Predicate P3 = P2 and functions P4 := P3 P2 and P5 := P2 + P3 are associated with t2 The firing of t1 by using <3,7> would produce the value 10 in P4. t2 can then fire using <4, 4> Ch. 5 61 Extension 2 specifying priorities • A priority function pri from transitions to natural numbers: • pri: T N • When several transitions are enabled, only the ones with maximum priority are allowed to fire • Among them, the one to fire is chosen nondeterministically Ch. 5 62 Extension 3 Timed Petri nets • A pair of constants <tmin, tmax> is associated with each transition • Once a transition is enabled, it must wait for at least tmin to elapse before it can fire • If enabled, it must fire before tmax has elapsed, unless it is disabled by the firing of another transition before tmax Ch. 5 63 Example combining priorities and time P 1 P t1 t m in = 1 tm a x = 4 p r io r it y = 1 P 2 P 3 t t 2 t m in = 2 tm a x = 3 p r io r it y = 3 Ch. 5 4 3 t m in = 0 tm a x = 5 p r io r it y = 2 64 Ori ginal m essage { tmi n = c1 tmax = k1 M essage trip li cati on M essage copi es tmi n = { tmax = c2 k2 M essage copi es transm ission PC2 PC3 PC1 { tmi n = 0 tmax = 0 tvoti ng1 tvoti ng2 tvoti ng3 for all three transi ti ons Precise specification of message triplication problem Case (1) Forwarded message Ch. 5 65 Ori ginal m essage tmi n = c1 tmax = k1 M essage trip li cati on M essage copi es tmi n = c2 tmax = k2 M essage copi es transm ission PC2 PC3 PC1 tmi n = 0 tmax = 0 Precise specification of message triplication problem Case (2) tvoti ng Forwarded message Ch. 5 66 Case study • An n elevator system to be installed in a building with m floors • Natural language specs contain several ambiguities • Formal specification using PNs removes ambiguities • Specification will be provided in a stepwise fashion • Will use modules, each encapsulating fragments of PNs which describe certain system components Ch. 5 67 From informal specs… “The illumination is cancelled when the elevator visits the floor and is either moving in the desired direction, or ...” 2 different interpretations (case of up call) – switch off as the elevator arrives at the floor from below (obvious restrictions for 1st and last floor) – switch off after the elevators starts moving up • in practice you may observe the two cases! Ch. 5 68 …more analysis of informal specs “The algorithm to decide which to service first should minimize the waiting time for both requests.” what does this mean? • in no other way can you satisfy either request in a shorter time – but minimizing for one may require longer for the other • the sum of both is minimal – why the sum? Ch. 5 69 Initial sketch of movement Ch. 5 70 Button module C P P ush 0 .0 5 . .0 .0 5 0 .1 . . On Set 0 . .0 O ff R eset Ch. 5 71 Elevator position (sketch) Fm UF F DF m-1 m-1 UF F 3 DF 3 3 UF 2 m-1 F2 DF 2 F1 Ch. 5 72 More precise description of elevator position F j+ 1 U F j+ 1 t8 t1 0 t7 UPh t9 t1 1 t1 2 On F j" t On DOW Nh F j' On IL B j+ 1 On t1 t2 t3 t4 t5 t6 IL B h On U P j+ 1 Fj D O W N j+ 1 On Ch. 5 Assume j+1hm 73 Switch internal button off Set IL B j 0..0 On O ff R e se t Fj Ch. 5 74 Switch external button off Fj' UPj Set ti' Fj On Off x..x Reset x time needed by a person to enter + pushing button Ch. 5 75 Specifying policy A “fair” solution: Keep the direction unchanged as long as there are calls that require elevator to go in that direction [x,x] U_D [0,0] DK UK [0,0] D U D_U [x,x] t7, t8, t9 have higher priority than t10, t11, t12 Ch. 5 76 A general scheduler SCHEDULER ... all transitions • Each transition has predicate OK(Scheduler) • Token in SCHEDULER stores information about the state of the system that is useful for scheduling transitions to fire • The token is “permanent” (it is always reproduced after the firing of any transition) Ch. 5 77 Declarative specifications ER diagrams: semiformal specs Logic specifications Algebraic specifications Ch. 5 78 ER diagrams • Often used as a complement to DFD to describe conceptual data models • Based on entities, relationships, attributes • They are the ancestors of class diagrams in UML Ch. 5 79 Example NAME AGE STUDENT SEX ENROLLED_IN SUBJECT CLASS COURSE_ID MAX_ENROLLMENT Ch. 5 80 Relations • Relations can be partial • They can be annotated to define – one to one A R B – one to many A R B – many to one A R B A R B – many to many Ch. 5 81 Non binary relations D u ratio n D ata D irecto r H ead O f D ep artm en t P articip ate A ssign ed P ro ject E m p lo yee Ch. 5 82 Logic specifications Examples of first-order theory (FOT) formulas: • x > y and y > z implies x > z • x=yy=x • for all x, y, z (x > y and y > z implies x > z) • x+1<x–1 • for all x (exists y (y = x + z)) • x > 3 or x < -6 Ch. 5 83 Specifying complete programs A property, or requirement, for P is specified as a formula of the type {Pre (i1, i2,..., in) } P {Post (o1, o2,..., om, i1, i2,..., in)} Pre: precondition Post: postcondition Ch. 5 84 Example • Program to compute greatest common divisor {i1 > 0 and i2 > 0} P {(exists z1, z2 (i1 = o * z1 and i2 = o * z2) and not (exists h (exists z1, z2 (i1 = h * z1 and i2 = h * z2) and h > o))} Ch. 5 85 Specifying procedures {n > 0} -- n is a constant value procedure search (table: in integer_array; n: in integer; element: in integer; found: out Boolean); {found (exists i (1 i n and table (i) = element))} {n > 0 } procedure reverse (a: in out integer_array; n: in integer); {for all i (1 i n) implies (a (i) = old–a (n - i +1))} Ch. 5 86 Specifying classes • Invariant predicates and pre/post conditions for each method • Example of invariant specifying an array implementing ADT set for all i, j (1 i length and 1 j length and ij) implies IMPL[i]IMPL[j] (no duplicates are stored) Ch. 5 87 Specifying non-terminating behaviors • Example: producer+consumer+buffer • Invariant specifies that whatever has been produced is the concatenation of what has been taken from the buffer and what is kept in the buffer input_sequence = append (output_sequence, contents(CHAR_BUFFER)) Ch. 5 88 A case-study using logic specifications • We outline the elevator example • Elementary predicates – at (E, F, T) • E is at floor F at time T – start (E, F, T, up) • E left floor F at time T moving up • Rules – (at (E, F, T) and on (EB, F1, T) and F1 > F) implies start (E, F, T, up) Ch. 5 89 States and events • Elementary predicates are partitioned into – states, having non-null duration – standing(E, F, T1, T2) » assumption: closed at left, open at right – events • instantaneous (caused state change occurs at same time) • represented by predicates that hold only at a particular time instant – arrived (E, F, T) • For simplicity, we assume • zero decision time • no simultaneous events Ch. 5 90 Events (1) • arrival (E, F, T) – E in [1..n], F in [1..m], T t0, (t0 initial time) • does not say if it will stop or will proceed, nor where it comes from • departure(E, F, D, T) – E in [1..n], F in [1..m], D in {up, down}, T t0 • stop (E, F, T) – E in [1..n], F in [1.. m], T t0 • specifies stop to serve an internal or external request Ch. 5 91 Events (2) • new_list (E, L, T) – E in [1..n], L in [1.. m]*, T t0 • L is the list of floors to visit associated with elevator (scheduling is performed by the control component of the system) • call(F, D, T) – external call (with restriction for 1, N) • request(E, F, T) – internal reservation Ch. 5 92 States • moving (E, F, D, T1, T2) • standing (E, F, T1, T2) • list (E, L, T1, T2) – We implicitly assume that state predicates hold for any sub- interval (i.e., the rules that describe this are assumed to be automatically added) • Nothing prevents that it holds for larger interval Ch. 5 93 Rules relating events and states R1:When E arrives at floor F, it continues to move if there is no request for service from F and the list is empty. If the floor to serve is higher, it moves upward; otherwise it moves downward. arrival (E, F, Ta) and list (E, L, T, Ta) and first (L) > F implies departure (E, F, up, Ta) A similar rule describes downward movement. Ch. 5 94 R2: Upon arrival at F, E stops if F must be serviced (F appears as first of the list) arrival (E, F, Ta) and list (E, L, T, Ta) and first (L) = F implies stop (E, F,Ta) R3: E stops at F if it gets there with an empty list arrival (E, F, Ta) and list (E, empty, T, Ta) implies stop (E, F, Ta) Ch. 5 95 R4: Assume that elevators have a fixed time to service a floor. If the list is not empty at the end of such interval, the elevator leaves the floor immediately. stop (E, F, Ta) and list (E, L, T, Ta + Dts) and first (L) > F, implies departure (E, F, up, Ta + Dts R5: If the elevator has no floors to service, it stops until its list becomes nonempty. stop (E, F, Ta) and list (E, L, Tp, T) and Tp > Ta + Dts and list (E, empty, Ta + Dts, Tp) and first (L) > F implies departure (E, F, up, Ch. Tp5) 96 R6: Assume that the time to move from on floor to the next is known and fixed. The rule describes movement. departure (E, F, up, T) implies arrival (E, F + 1, T + Dt) R7: The event of stopping initiates standing for at least Dts. stop (E, F, T) implies standing (E, F, T, T + Dts) Ch. 5 97 R8: At the end of the minimum stop interval Dts, E remains standing if there are no floors to service. stop (E, F, Ts) and list (E, empty, Ts + Dts, T) implies standing (E, F, Ts, T) R9: Departure causes moving. departure (E, F, D, T) implies moving (E, F, D, T, T + Dt) Ch. 5 98 Control rules Express the scheduling strategy (by describing “new_list” events and “list” states) Internal requests are inserted in the list from current floor to top if the elevator is moving up External calls are inserted in the list of the closest elevator that is moving in the correct direction, or in a standing elevator Ch. 5 99 R10: Reserving F from inside E, which is not standing at F, causes immediate update of L according to previous policy request (E, F, TR) and not (standing (E, F, Ta, TR)) and list (E, L, Ta, TR) and LF = insert_in_order(L, F, E) implies new_list (E, LF, TR) Ch. 5 100 R11: Effect of arrival of E at floor F arrival (E, F, Ta) and list (E, L, T, Ta) and F = first (L) and Lt = tail (L) implies new_list (E, Lt, Ta) R12: How list changes new_list (E, L, T1) and not (new_list (E, L, T2) and T1 < T2 < T3) implies list (E, L, T1, T3) Ch. 5 101 Verifying specifications • The system can be simulated by providing a state (set of facts) and using rules to make deductions standing (2, 3, 5, 7) elevator 2 at floor 3 at least from instant 5 to 7 list(2, empty, 5, 7) request(2, 8, 7) new_list(2, {8}, 7) (excluding other events) departure (2, up, 7 + Dts) arrival (2, 8, 7 + Dts + Dta *(8-3)) Ch. 5 102 Verifying specifications • Properties can be stated and proved via deductions new_list (E, L, T) and F L implies new_list (E, L1, T1) and F L1 and T1 > T2 (all requests are served eventually) Ch. 5 103 Descriptive specs • The system and its properties are described in the same language • Proving properties, however, cannot be fully mechanized for most languages Ch. 5 104 Algebraic specifications • Define a heterogeneous algebra • Heterogeneous = more than 1 set • Especially useful to specify ADTs Ch. 5 105 Example • A system for strings, with operations for – creating new, empty strings (operation new) – concatenating strings (operation append) – adding a new character at the end of a string (operation add) – checking the length of a given string (operation length) – checking whether a string is empty (operation isEmpty) – checking whether two strings are equal (operation equal) Ch. 5 106 Specification: syntax algebra StringSpec; introduces sorts String, Char, Nat, Bool; operations new: () String; append: String, String String; add: String, Char String; length: String Nat; isEmpty: String Bool; equal: String, String Bool Ch. 5 107 Specification: properties constrains new, append, add, length, isEmpty, equal so that for all [s, s1, s2: String; c: Char] isEmpty (new ()) = true; isEmpty (add (s, c)) = false; length (new ()) = 0; length (add (s, c)) = length (s) + 1; append (s, new ()) = s; append (s1, add (s2,c)) = add (append (s1,s2),c); equal (new (),new ()) = true; equal (new (), add (s, c)) = false; equal (add (s, c), new ()) = false; equal (add (s1, c), add (s2, c) = equal (s1,s2); end StringSpec. Ch. 5 108 Example: editor • newF – creates a new, empty file • isEmptyF – states whether a file is empty • addF – adds a string of characters to the end of a file • insertF – inserts a string at a given position of a file (the rest of the file will be rewritten just after the inserted string) • appendF – concatenates two files Ch. 5 109 algebra TextEditor; introduces sorts Text, String, Char, Bool, Nat; operations newF: () Text; isEmptyF: Text Bool; addF: Text, String Text; insertF: Text, Nat, String Text; appendF: Text, Text Text; deleteF: Text Text; lengthF : Text Nat; equalF : Text, Text Bool; addFC: Text, Char Text; {This is an auxiliary operation that will be needed to define addF and other operations on files.} Ch. 5 110 constrains newF, isEmptyF, addF, appendF, insertF, deleteF so that TextEditor generated by [newF, addFC] for all [f, f1,f2: Text; s: String; c: Char; cursor: Nat] isEmptyF (newF ()) = true; isEmptyF (addFC (f, c)) = false; addF (f, newS ()) = f; addF (f, addS (s, c)) = addFC (addF (f, s), c); lengthF (newF ()) = 0; lengthF (addFC (f, c)) = lengthF (f) + 1; appendF (f, newF ()) = f; appendF (f1, addFC (f2, c)) = addFC (appendF (f1, f2), c); equalF (newF (),newF ()) = true; equalF (newF (), addFC (f, c)) = false; equalF (addFC (f, c), new ()) = false; equalF (addFC (f1, c1), addFC (f2, c2) = equalF (f1, f2) and equalC (c1, c2); insertF (f, cursor, newS ()) = f; ((equalF (f, appendF (f1, f2)) and (lengthF (f1) = cursor - 1)) implies equalF (insertF (f, cursor, s), appendF (addF (f1, s), f2))) = true; end TextEditor. Ch. 5 111 Requirements for a notation • Ability to support separation of concerns – e.g., separate functional specs from • performance specs • user-interface specs •… • Support different views Ch. 5 112 Example of views document production data flow view (1) Predefined Text skeletons Predefined Formats User Formatting options Customer data (name, type of document) Docum ent production Customers Print Docum ent Ch. 5 113 Control flow view (2) Get user nam e Search i n Customers Get other d ata from the data base Get approp ri ate text skeletons from predefi ned text l ibrary Get other rel evant data from user interacti on Comp ose the docume nt by choosi ng form atting opti ons (thi s i nvol ves interacti on wi th the user and access to the Formats data base) Pri nt docum ent (b) Ch. 5 114 UML notations • Class diagrams – describe static architecture in terms of classes and associations – dynamic evolution can be described via Statecharts (see later) • Activity diagrams – describe sequential and parallel composition of method executions, and synchronization Ch. 5 115 An activity diagram [c1 ] A [c3 ] E [c4 ] [c2 ] (1 ) F B C D G end (2 ) Ch. 5 116 Building modular specifications • The case of algebraic specifications – How to combine algebras taken from a library – How to organize them in a hierarchy Ch. 5 117 Algebras used by StringSpec algebra BoolAlg; introduces sorts Bool; operations true () Bool; false () Bool; not : Bool Bool; and: Bool, Bool Bool; or: Bool, Bool Bool; implies: Bool, Bool Bool; : Bool, Bool Bool; constrains true, false, not, and, or, implies, so that Bool generated by [true, false] for all [a, b: Bool] not (true) = false; not (false) = true; a and b = not (not (a) or not (b)); a implies b = not (a) or b; … end BoolAlg. Ch. 5 118 Algebras used by StringSpec (cont.) algebra NatNumb; introduces sorts Nat, Bool; operations 0: () Nat; Succ: Nat Nat; + : Nat, Nat Nat; - : Nat, Nat Nat; = : Nat, Nat Bool; … constrains 0, Succ, +, -, =,..., so that NatNumb generated by [0, Succ] … end NatNumb. Ch. 5 algebra CharAlg; introduces sorts Char, Bool; operations ‘a’: ()® Char; ‘b’ : ()® Char; … end CharAlg. 119 StringSpec revisited algebra StringSpec; imports BoolAlg, NatNumb, CharAlg; introduces sorts String, Char, Nat, Bool; operations new: () String; … end StringSpec. Ch. 5 120 Incremental specification of an ADT • We want to target stacks, queues, sets • We start from "container" and then progressively specialize it • We introduce another structuring clause – assumes • defines inheritance relation among algebras Ch. 5 121 Container algebra algebra Container; imports DataType, BoolAlg, NatNumb; introduces sorts Cont; operations new: () Cont; insert: Cont, Data Cont; {Data is the sort of algebra DataType, to which elements to be stored in Cont belong} isEmpty: Cont Bool; size: Cont Nat; constrains new, insert, isEmpty, size so that Cont generated by [new, insert] for all [d: Data; c: Cont] isEmpty (new ()) = true; isEmpty (insert (c, d)) = false; size (new ()) = 0; end Container. Ch. 5 122 Table specializes Container algebra TableAlg; assumes Container; introduces sorts Table; operations last: Table Data; rest: Table Table; equalT : Table, Table Bool; delete: Table, Data Table; constrains last, rest, equalT, delete, isEmpty, new, insert so that for all [d, d1, d2: Data; t, t1, t2: Table] last (insert (t, d)) = d; rest (new ()) = new (); rest (insert (t, d)) = t; equalT (new (), new ()) = true; equalT (insert (t, d), new ()) = false; equalT (new (), insert (t,d)) = false; equalT (t1,t2) = equalD(last (t1), last (t2)) and equalT (rest (t1),rest (t2)); delete (new (), d) = new (); delete (insert (t,d),d) = delete (t, d); if not equalD(d1, d2) then Ch. 5(delete (t, d2), d1); delete (insert (t, d1), d2) = insert end TableAlg. 123 Queue specializes Container algebra QueueAlg; assumes Container; introduces sort Queue; operations last: Queue Data; first: Queue Data; equalQ : Queue , Queue Bool; delete:Queue Queue; constrains last, first, equalQ, delete, isEmpty, new, insert so that for all [d: Data; q, q1, q2: Queue] last (insert (q, d)) = d; first (insert (new(), d) = d first (insert (q, d)) = if not isEmpty (q) then first (q); equalQ (new (), new ()) = true; equalQ (insert (q, d), new ()) = false; equalQ (new (), insert (q, d)) = false; equalQ (insert (q1, d1), insert (q2, d2)) = equalD (d1, d2) and equalQ (q1,q2); delete (new ()) = new (); delete (insert (new (), d)) = new (); if not equalQ (q, new ()) then delete (insert (q,d)) = insert (delete (q), d); Ch. 5 end QueueAlg. 124 A graphical view Queue Algebra Table Algebra Container Algebra Bool Algebra Legend: Nat Algebra DataType Algebra imports relation assumes relation Ch. 5 125 A richer hierarchy Set M ultiset Sorted T able T ree Queue Algeb ra T able Algeb ra Conta iner Algeb ra Sorted DataT ype Array Algeb ra Bool Algeb ra Nat Algeb ra Ch. 5 DataT ype Algeb ra 126 From specs to an implementation • Algebraic spec language described so far is based on the "Larch shared language" • Several "interface languages" are available to help transitioning to an implementation – Larch/C++, Larch/Pascal Ch. 5 127 Using Larch/Pascal for StringSpec type String exports isEmpty, add, append,... based on Boolean, integer, character function isEmpty (s: String) : Boolean modifies at most [ ] {i.e., it has no side effects}; procedure add (var s : String; c : char) modifies at most [s] {modifies only the string parameter s}; function length (s: String) : integer modifies at most [ ] ; procedure append (var s1, s2, s3: string) modifies at most [s3] {only s3, the result of the operation, is modified}; end StringSpec. Ch. 5 128 Modularizing finite state machines • Statecharts do that • They have been incorporated in UML • They provide the notions of – superstate – state decomposition Ch. 5 129 Sequential decomposition --chemical plant control example-N o rm a l A n o m a ly D etectio n R eco v ery S u ccess R eco v ery P ress R eco v ery Id en tifica tio n T em p D one P ressu re A ctio n D one T em p era tu re A ctio n Ch. 5 R eco v ery F a ilu re 130 Parallel decomposition Idle start stop C oncurrentW ork w rite 1 P1 w rite C1 read produce 0 read read w rite 2 P2 P roducer B uffer Ch. 5 consum e C2 C onsum er 131 Object state diagram using Statecharts Top Push(item) Empty NotEmpty y Pop[stack contains 1 item] Push(item) Pop[stack contains more than 1 item] Ch. 5 132 Modularizing logic specifications: Z • System specified by describing state space, using Z shemas • Properties of state space described by invariant predicates – predicates written in first-order logic • Operations define state transformations Ch. 5 133 The elevator example in Z Ch. 5 134 Complete state space attempt #1 Ch. 5 135 Complete state space attempt #2 Ch. 5 136 Complete state space final Ch. 5 137 Operations (1) Ch. 5 138 Operations (2) Ch. 5 139 Specifications for the end-user • Specs should be used as common reference for producer and user • They help removing ambiguity, incompleteness, … • Can they be understood by end-user? – They can be the starting point for a prototype – They can support some form of animation (e.g., see Petri nets) Ch. 5 140 Conclusions (1) • Specifications describe – what the users need from a system (requirements specification) – the design of a software system (design and architecture specification) – the features offered by a system (functional specification) – the performance characteristics of a system (performance specification) – the external behavior of a module (module interface specification) – the internal structure of a module (internal structural specification) Ch. 5 141 Conclusions (2) • Descriptions are given via suitable notations – There is no “ideal” notation • They must be modular • They support communication and interaction between designers and users Ch. 5 142

Descargar
# Specification - Higher Education | Pearson