Lecture 10: Descriptive SpecificationsKenneth M. AndersonFoundations of Software EngineeringCSCI 5828 - Spring Semester, 2000February 17, 2000 ' Kenn eth M. Anderson, 2000 2Today s Lecture¥ Introduce Descriptive Specifications—E-R Diagrams (Semi-Formal)—Axiomatic—Algebraic—Tour of the RAISE system¥ Developed in Denmark¥ Sold to European Manufacturing companies¥ Using RAISE to create these types of specifications—Has a full tool suiteFebruary 17, 2000 ' Kenn eth M. Anderson, 2000 3Descriptive Specifications¥ Focuses on Properties—Describes the desired properties of a systemrather than its desired behavior¥ Formalisms—Axiomatic (Logic)—AlgebraicFebruary 17, 2000 ' Kenn eth M. Anderson, 2000 4Formalisms Provide Preciseness¥ Use of Mathematical Formalisms—Properties are specified precisely by buildingon top of the precise mathematical syntax andsemantics of the underlying formalisms¥ Mathematical Foundations—Predicate logic, set theory, abstract algebraFebruary 17, 2000 ' Kenn eth M. Anderson, 2000 5Entity-Relationship Diagrams¥ A semi-formal notation for describing thestructure and relationships of data—Akin to how Data Flow Diagrams are a semi-formalnotation for describing the operations that access andmanipulate data¥ Problems—Syntax and Semantics are not precisely defined—Lack of Expressive power¥ requires the use of natural language annotationsFebruary 17, 2000 ' Kenn eth M. Anderson, 2000 6Example ER Diagram(taken from textbook page 200)Enrolled_InNameAgeSexSubjectCourse_IDMax_EnrollmentClassStudentFebruary 17, 2000 ' Kenn eth M. Anderson, 2000 7ER Diagrams and UML¥ ER Diagrams can be seen as precursors toUML s Class Diagrams¥ Differences—operations and inheritance are added¥ Advantages—ER notation was never standardized, UML sclass diagrams provide a standard notation¥ however, remember that they are both semi-formalFebruary 17, 2000 ' Kenn eth M. Anderson, 2000 8Logic Specifications¥ Vocabulary of Logical Expressions—Variables, constants, predicates, functions—Connectives: and (∧), or (∨), not (¬),implies (⇒), equivalent (≡)—Quantifiers: exists (∃), for all (∀)¥ Combined with Vocabulary of Application—Example: set operators (∈, ∪, ∩, )—Example: ADT operators (Push, IsFull, )February 17, 2000 ' Kenn eth M. Anderson, 2000 9Logic Specifications¥ Examples—x > y and y > z implies x > z—for all x (exists y (y = x + z))¥ Additional Notes—Variables are either free or bound¥ A formula with all variables bound is called closed; closedformulas are always either true or false—Expressions are theories in the logic—V&V amounts to theorem provingFebruary 17, 2000 ' Kenn eth M. Anderson, 2000 10Creating Logic Specifications¥ Helper Predicates and Functions—Define the base properties of interest¥ Used as a domain-specific vocabulary—Modularize the specification¥ e.g., defined in one spec; used in another¥ Examples—height(bob) = 72; tall(bob)—for p: person (height(p)>60 implies tall(p))February 17, 2000 ' Kenn eth M. Anderson, 2000 11Logic Specification Techniques¥ Preconditions andPostconditions—Textbook gives lots ofexamples on 204-205Assume <i1, i2, i3, >are input valuesAssume <o1, o2, o3, >are output values¥ A property is defined{Pre(i1, i2, i3, )}P{Post(o1, o2, o3, , i1,i2, i3, >}¥ Example{exists z (i1 = z * i2)}P{o1 = i1/i2}February 17, 2000 ' Kenn eth M. Anderson, 2000 12Logic Specification Techniques¥ Invariants and Assertions—Logic specs are used to assert properties ofportions of code as well—For instance, to assert something that is alwaystrue of a routine or to record the assumptionsabout variables passed to a procedure{n > 0}procedure reverse (a: in out int_array; n: in int){for all i (1<=i<=n) implies (a(i) = old_a(n-i+1))}February 17, 2000 ' Kenn eth M. Anderson, 2000 13Algebraic Specifications¥ Make use of heterogeneous algebra—a collection of different sets on which severaloperations are defined—Traditional algebras are homogeneous, one setand a several operations; e.g. integers—Heterogeneous algebras contain multiple sets¥ e.g. length( ken ) = 3¥ Here we have the set of strings and integers with oneoperation length definedFebruary 17, 2000 ' Kenn eth M. Anderson, 2000 14RAISE¥ A Method and a Language¥ Specification Language: RSL¥ Specifications Refined in Levels—Associated consistency proof obligations¥ Proofs of Properties Aided by ToolsRigorous Approach to Industrial Software EngineeringFebruary 17, 2000 ' Kenn eth M. Anderson, 2000 15Background Information¥ In RAISE, they make use of a funny notionof the domain and range of a function¥ Each function consists of a set of tuples.The domain is the set of elements that makeup the first element of each tuple; the rangeis the set of elements that make up thesecond set of each tupleFebruary 17, 2000 ' Kenn eth M. Anderson, 2000 16Example¥ S = {}¥ S = S‘ [1 |-> 2]¥ S = S‘ [3 |-> 4]¥ S = S‘ \[1]¥ Empty Set¥ S = {(1,2)}¥ Domain = {1}¥ Range = {2}¥ S = {(1,2), (3,4)}¥ Domain = {1, 3}¥ Range = {2, 4}¥ S = {(3, 4)}February 17, 2000 ' Kenn eth M. Anderson, 2000 17RAISE Specification of POTS** Plain Old Telephone ServiceFebruary 17, 2000 ' Kenn eth M. Anderson, 2000 18scheme POTS =RAISE Specification of POTSFebruary 17, 2000 ' Kenn eth M. Anderson, 2000 19scheme POTS =classtype value variable RAISE Specification of POTSFebruary 17, 2000 ' Kenn eth M. Anderson, 2000 20scheme POTS =classtypeRAISE Specification of POTSFebruary 17, 2000 ' Kenn eth M. Anderson, 2000 21scheme POTS =classtype Line, RAISE Specification of POTSFebruary 17, 2000 ' Kenn eth M. Anderson, 2000 22scheme POTS =classtype Line, Status = Line {On_Hook, Off_Hook}, RAISE Specification of POTSm→ February 17, 2000 ' Kenn eth M. Anderson, 2000 23scheme POTS =classtype Line, Status = Line {On_Hook, Off_Hook}, Calls = Line LineRAISE Specification of POTSm→ m→ February 17, 2000 ' Kenn eth M. Anderson, 2000 24scheme POTS =classtype Line, Status = Line {On_Hook, Off_Hook}, Calls = Line LinevalueRAISE Specification of POTSm→ m→February 17, 2000 ' Kenn eth M. Anderson, 2000 25scheme POTS =classtype Line, Status = Line {On_Hook, Off_Hook}, Calls = Line Linevalue go_off_hook : Line → Unit, RAISE Specification of POTSm→ m→ February 17, 2000 ' Kenn eth M. Anderson, 2000 26scheme POTS =classtype Line, Status = Line {On_Hook,
View Full Document
Unlocking...