Today s Lecture Introduce Descriptive Specifications E R Diagrams Semi Formal Axiomatic Algebraic Tour of the RAISE system Lecture 10 Descriptive Specifications Kenneth M Anderson Foundations of Software Engineering CSCI 5828 Spring Semester 2000 Developed in Denmark Sold to European Manufacturing companies Using RAISE to create these types of specifications Has a full tool suite February 17 2000 Focuses on Properties Use of Mathematical Formalisms Describes the desired properties of a system rather than its desired behavior Properties are specified precisely by building on top of the precise mathematical syntax and semantics of the underlying formalisms Formalisms Mathematical Foundations Axiomatic Logic Algebraic Kenn eth M Anderson 2000 2 Formalisms Provide Preciseness Descriptive Specifications February 17 2000 Kenn eth M Anderson 2000 Predicate logic set theory abstract algebra 3 February 17 2000 Kenn eth M Anderson 2000 4 Entity Relationship Diagrams Example ER Diagram A semi formal notation for describing the structure and relationships of data Student Akin to how Data Flow Diagrams are a semi formal notation for describing the operations that access and manipulate data Name Age Sex Problems Class Enrolled In Subject Course ID Max Enrollment Syntax and Semantics are not precisely defined Lack of Expressive power taken from textbook page 200 requires the use of natural language annotations February 17 2000 Kenn eth M Anderson 2000 5 February 17 2000 ER Diagrams and UML Vocabulary of Logical Expressions Variables constants predicates functions Connectives and or not implies equivalent Quantifiers exists for all operations and inheritance are added Advantages Combined with Vocabulary of Application ER notation was never standardized UML s class diagrams provide a standard notation Example set operators Example ADT operators Push IsFull however remember that they are both semi formal Kenn eth M Anderson 2000 6 Logic Specifications ER Diagrams can be seen as precursors to UML s Class Diagrams Differences February 17 2000 Kenn eth M Anderson 2000 7 February 17 2000 Kenn eth M Anderson 2000 8 Logic Specifications Creating Logic Specifications Examples Helper Predicates and Functions x y and y z implies x z for all x exists y y x z Define the base properties of interest Used as a domain specific vocabulary Additional Notes Modularize the specification Variables are either free or bound e g defined in one spec used in another A formula with all variables bound is called closed closed formulas are always either true or false Examples Expressions are theories in the logic V V amounts to theorem proving February 17 2000 Kenn eth M Anderson 2000 height bob 72 tall bob for p person height p 60 implies tall p 9 Logic Specification Techniques Preconditions and Postconditions Textbook gives lots of examples on 204 205 Assume i1 i2 i3 are input values Assume o1 o2 o3 are output values February 17 2000 Kenn eth M Anderson 2000 10 Logic Specification Techniques A property is defined Invariants and Assertions Pre i1 i2 i3 P Post o1 o2 o3 i1 i2 i3 Logic specs are used to assert properties of portions of code as well For instance to assert something that is always true of a routine or to record the assumptions about variables passed to a procedure Example exists z i1 z i2 P o1 i1 i2 Kenn eth M Anderson 2000 February 17 2000 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 11 February 17 2000 Kenn eth M Anderson 2000 12 Algebraic Specifications RAISE Make use of heterogeneous algebra Rigorous Approach to Industrial Software Engineering a collection of different sets on which several operations are defined Traditional algebras are homogeneous one set and a several operations e g integers Heterogeneous algebras contain multiple sets A Method and a Language Specification Language RSL Specifications Refined in Levels e g length ken 3 Here we have the set of strings and integers with one operation length defined February 17 2000 Kenn eth M Anderson 2000 13 Associated consistency proof obligations Proofs of Properties Aided by Tools February 17 2000 Background Information S S S 1 2 S S 3 4 S S 1 Kenn eth M Anderson 2000 14 Example In RAISE they make use of a funny notion of the domain and range of a function Each function consists of a set of tuples The domain is the set of elements that make up the first element of each tuple the range is the set of elements that make up the second set of each tuple February 17 2000 Kenn eth M Anderson 2000 15 February 17 2000 Empty Set S 1 2 Domain 1 Range 2 S 1 2 3 4 Domain 1 3 Range 2 4 S 3 4 Kenn eth M Anderson 2000 16 RAISE Specification of POTS RAISE Specification of POTS scheme POTS Plain February 17 2000 Old Telephone Service Kenn eth M Anderson 2000 17 RAISE Specification of POTS February 17 2000 Kenn eth M Anderson 2000 18 RAISE Specification of POTS scheme POTS class type scheme POTS class type value variable February 17 2000 Kenn eth M Anderson 2000 19 February 17 2000 Kenn eth M Anderson 2000 20 RAISE Specification of POTS RAISE Specification of POTS scheme POTS class type Line February 17 2000 Kenn eth M Anderson 2000 scheme POTS class type Line Status Line m On Hook Off Hook 21 RAISE Specification of POTS Kenn eth M Anderson 2000 Kenn eth M Anderson 2000 22 RAISE Specification of POTS scheme POTS class type Line Status Line m On Hook Off Hook Line Calls Line m February 17 2000 February 17 2000 scheme POTS class type Line Status Line m On Hook Off Hook Line Calls Line m value 23 February 17 2000 Kenn eth M Anderson 2000 24 RAISE Specification of POTS RAISE Specification of POTS scheme POTS class type Line Status Line m On Hook Off Hook Calls Line m Line value go off hook Line Unit February 17 2000 Kenn eth M Anderson 2000 scheme POTS class type Line Status Line m On Hook Off Hook Calls Line m Line value go off hook Line Unit go on hook Line Unit 25 RAISE Specification of POTS Kenn eth M Anderson 2000 Kenn eth M Anderson 2000 26 RAISE Specification of POTS scheme POTS class type Line Status Line m On Hook Off Hook Line Calls Line m value go off hook Line Unit go on hook Line Unit place call Line Line Bool February 17 2000 February 17 2000 scheme POTS class type Line Status Line m On Hook Off Hook Line Calls Line m value go off hook Line Unit go on hook Line Unit place call Line Line Bool end call Line Unit 27 February 17 2000 Kenn eth M Anderson 2000 28 RAISE Specification of POTS RAISE Specification of POTS
View Full Document
Unlocking...