csa2070 Formal slides

Formal Specification: 

Formal Specification A Very First Acquaintance

What is Formal Specification: 

What is Formal Specification The application of set theory, propositional and predicate calculi to the specification of systems.

Sets: 

Sets Are collections of elements Are represented by standard notation Are manipulated by standard elementary operations Are entities which can interact with each other

Examples of Sets: 

Examples of Sets Notation: { } Set of colours: {green,blue,yellow} Set of sports: {tennis,football, equestrian} Set of BCIS SEM tutors: {ernest} Empty set: { } or 

Set Construction: 

Set Construction In notational form (aka comprehensive specification): {Signature | Predicate • Term} Direct (as in previous slide) Operations on other sets according to the form: The resulting set whose elements are formed by the operation on elements selected by the condition from the original set with elements from range. Translates to…

Set Construction Examples: 

Set Construction Examples Alternate even numbers: { x : N | x mod 2 = 0 ∙ 2 * x } = {0,4,8,12,16,20,…} Tens: { x : N | x ∙ 10 * x } = {0,10,20,30,40,…} Squares of multiples of 4 (excluding zero): { x : Z | (x mod 4 = 0)  (x > 0) ∙ x * x } = {16,64,144,256,…}

Some Set-Based Specification Exercises: 

Some Set-Based Specification Exercises Write 3 elements from the sets specified by the following comprehensive specifications: {n : N | n < 20  n > 10 • n} {n : N | n3 > 10 • n} {x,y : N | x + y = 100 • (x,y)} {x,y : N | x + y = 5 • x2 + y2} Interpret the following: {m : monitors | MonitorState(m, on) • m} {f : SysFiles | f  DelFiles  f  ArcFiles • f} Write the comprehensive specification of: {(10,100),(11,121),(12,144),(13,169),(14,196)}

Set Operators: 

Set Operators Operator list in NCC slide and handout (notes). Examples: Mosta  {Maltese towns} London  {Maltese towns} #{joe,veronica,mark} = 3 {paul,richard,claire,george}  {Group B} IP{milan,juve} = { { },{milan},{juve},{milan,juve} } {dobie,collie,poodle}  {poodle,labrador} = {dobie,collie,poodle,labrador} {dobie,collie,poodle}  {poodle,labrador} = {poodle} {dobie,collie,poodle} \ {poodle,labrador} = {dobie,collie}

Propositional Calculus: 

Propositional Calculus Deals with logic Basically consists of statements which can be true or false (Excluded Middle Law) Are mutually exclusive - never true or false at the same time (Contradiction Law) Is fundamental Is axiomatic In theory, can be used to describe anything

Proposition (and not) Examples: 

Proposition (and not) Examples Some birds can fly The nation Malta is in Asia Dogs are mammals All fish live in water All fish live in sea water Monique is the only lady in our group Cikku qatt ma jgorr Sit down. How are you today? Get my tea, please. What is the weather like? ARE ARE NOT

Representing Propositions: 

Representing Propositions Consider the following… 10 is greater than 8 8 is less than 10 8 < 10 10 > 8 There is a positive number such that if we add it to eight the result would be ten. All the above are one and the same proposition

Propositional Calculus Notation: 

Propositional Calculus Notation Please refer to the R. Pressman textbook, or any other Software Engineering textbook containing basic formal specification, for a listing of basic propositional operators.

Examples to Discuss: 

Examples to Discuss Taking: P as true Q as false R as false S as true Answers: TRUE FALSE FALSE FALSE Click again for answers…

Contradictions and Tautologies: 

Contradictions and Tautologies A contradiction is a proposition that is always false for all possible values and variables making it up A tautology is a proposition that is always true for all possible values and variables making it up Examples:

De Morgan’s Laws: 

De Morgan’s Laws The above can be summarised (in Maltese) as follows: Jekk mhux abjad u iswed (it-tnejn me]udin f’daqqa) ifisser li mhux abjad jew mhux iswed. Mentri, jekk mhux abjad jew iswed (l-ebda wa]da minnhom) ifisser li mhux abjad u mhux iswed. …g]a[nuha ftit f’mo]]kom!

Specifying with Propositions: 

Specifying with Propositions Consider the following text: The system is in alert state only when it is waiting for an intruder and is on practice alert. alert  waiting  practice If the system is in teaching mode and is on practice alert, then it is in alert state. teaching  practice  alert The system will be in teaching mode and on practice alert and not waiting for an intruder. teaching  practice  ¬ alert Therefore…

Detecting Contradictions: 

Detecting Contradictions From the previous system: alert  waiting  practice teaching  practice  alert teaching  practice  ¬alert The second and third propositions yield a contradiction: teaching  practice  alert teaching  practice  ¬alert alert  ¬alert …contradiction! The first proposition yields another contradiction: teaching  practice  ¬(waiting  practice) eventually simplifies to… alert  ¬waiting …contradiction because alert requires waiting!

Predicate Calculus: 

Predicate Calculus Can be viewed as conditional statements obeying propositional behaviour with specific values. Consider a triangle… We can say the following… Any side will be greater than zero length; The sum of the length of any two sides will be greater than the length of the remaining side. Therefore… a b c

Predicate Calculus Example (clarified from NCC material): 

Predicate Calculus Example (clarified from NCC material) In predicate calculus form the basic properties of a triangle could be written as follows: Property 1 Property 2

Consider This Statement: 

Consider This Statement Fido is a dog, dogs like bones so Fido likes bones. Propositional analysis of this sentence yields: Fido is a dog (propos. 1) P Dogs like bones (propos. 2) Q Fido likes bones (propos. 3) R Can we derive R from P and Q using only propositional calculus? – No! Therefore…

We Introduce “A Predicate”: 

We Introduce “A Predicate” Formally a predicate can be seen as direct indicators of object properties. Examples of unary predicates: dog(fido) =true; dog(lecturer) =false Examples of n-ary predicates: father(john,mary) team(pawlu,bertu,`ensu)

A More Familiar Predicate Form: 

A More Familiar Predicate Form Consider the predicates: numerically_bigger_than(x,y) are_equal(a,b) Can be written as… x > y a = b

Quantification: 

Quantification Places bounds on free variables (i.e. names of objects) Is a unary predicate Are propositions There exists an object ‘x’ to which the predicate ‘P(x)’ applies. For all objects ‘x’, the predicate ‘P(x)’ applies.

Quantification Examples: 

Quantification Examples

Say the Following in Natural Language (loosely adopted from Behforooz, A.): 

Say the Following in Natural Language (loosely adopted from Behforooz, A.) All numeric values x, y, and z for which x is greater than y and y is greater than z, x is greater than z There exists a numeric value x, such that either x is greater than 10 or for some value y the sum of x and y is less than 100 If x and y are natural numbers, then x+y is also a natural number There exist x and y from the set {1,2,3,4} such that the sum of x and y is also a member of the set {1,2,3,4} For all values x and y from the set {1,2,3,4} for which x is greater than y, the difference between x and y is also an element of the set {1,2,3,4} The complement (negation of) two logical AND-ed values is the same as the complement of each OR-ed value The numeric value x is greater than y if and only if the difference between x and y is positive If the sum of x and y is positive, it cannot be concluded that both x and y are positive

Algebraic Specifications: 

Algebraic Specifications A specification technique mainly used for abstract data types Based on a strong mathematical foundation – namely algebra Have been in use for relatively long periods of time Are universal in their application Employ fundamental principles

Building Algebraic Specifications: 

Building Algebraic Specifications Clearly comprehend the system to model Determine the operations necessary for the system you have in mind Specify the relationship between the system’s operations Write the specification down according to adopted standard (a popular standard is the Common Algebraic Specification Language – CASL)

Algebraic Specification Queue Example (1/2) (loosely adopted from Pressman, R. S.): 

Algebraic Specification Queue Example (1/2) (loosely adopted from Pressman, R. S.) A message queue: Operations: add an item [AddItem] remove an item [RemItem] check if empty [IsEmpty] get first queue item [GetFirst] get last item [GetLast] create a new queue [Create]

Algebraic Specification Example (2/2) (loosely adopted from Pressman, R. S.): 

Algebraic Specification Example (2/2) (loosely adopted from Pressman, R. S.) Type: queue(Z) Imports: Boolean Signatures: Create  queue(Z) AddItem(Z,queue(Z))  queue(Z) RemItem(Z,queue(Z))  queue(Z) GetFirst(queue(Z))  Z GetLast(queue(Z))  Z IsEmpty(queue(Z))  Boolean Axioms: IsEmpty(Create)=true IsEmpty(AddItem(z,q))=false RemItem(AddItem(z,q),q)=q GetLast(AddItem(z,q))=z GetFirst(AddItem(z,Create)=z

Algebraic Specification Table Example (1/4) (loosely adopted from Pressman, R. S.): 

Algebraic Specification Table Example (1/4) (loosely adopted from Pressman, R. S.) A symbol table: Operations: create a new empty table [Create] add an item [AddItem] remove an item [RemItem] check if a symbol is in a table [InTab] join two tables [Join] get common symbols [Common] check if two tables are identical [IsEqual] check if a table is part of another [IsPartof] check is a table is empty [IsEmpty]

Algebraic Specification Table Example (2/4) (loosely adopted from Pressman, R. S.): 

Algebraic Specification Table Example (2/4) (loosely adopted from Pressman, R. S.) Signatures: Create  table(Z) AddItem(Z,table(Z))  table(Z) RemItem(Z,table(Z))  table(Z) InTab(Z,table(Z))  Boolean IsPartOf(table(Z),table(Z))  Boolean IsEqual(table(Z),table(Z))  Boolean IsEmpty(table(Z))  Boolean Join(table(Z),table(Z))  table(Z) Common(table(Z),table(Z))  table(Z)

Algebraic Specification Table Example (3/4) (loosely adopted from Pressman, R. S.): 

Algebraic Specification Table Example (3/4) (loosely adopted from Pressman, R. S.) Some applicable axioms (1): AddItem(s2,AddItem(s1,s))=if s1=s2 then AddItem(s1,s) else AddItem(s1,AddItem(s2,s)) RemItem(s1,Create)=Create RemItem(s1,AddItem(s2,s))=if s1=s2 then RemItem(s1,s) else AddItem(s2,RemItem(s1,s)) InTab(s1,Create)=false InTab(s1,AddItem(s2,s))=if s1=s2 then true else InTab(s1,s) Join(s,Create)=s Join(s, AddItem(s1,t))=AddItem(s1,Join(s,t))

Algebraic Specification Table Example (4/4) (loosely adopted from Pressman, R. S.): 

Algebraic Specification Table Example (4/4) (loosely adopted from Pressman, R. S.) Some applicable axioms (2): Common(s,Create)=Create Common(s,AddItem(s1,t))=if InTab(s1,s) then AddItem(s1,common(s,t)) else common(s,t) IsPartOf(Create,s)=true IsPartOf(AddItems(s1,s),t)=if InTab(s1,t) then IsPartOf(s,t) else false IsEqual(s,t)=IsPartOf(s,t)IsPartOf(t,s) IsEmpty(Create)=true IsEmpty(AddItem(s1,t))=false

“Club” Example: 

“Club” Example “Club” example will be discussed during lectures.

The Z-Specification Language: 

The Z-Specification Language Attempts to place a notational framework on formal system specification Based on set theory Is model-based (relies on well understood mathematical entities and their relationship) Equally used to model (specify) state as well as operations on states

Some Basic Z-Schema Examples (1/2): 

Some Basic Z-Schema Examples (1/2) a is a natural number and b is a set formed of natural numbers as shown. a is contained in b. Note: Generically, to indicate “a set of”, the notation “P (with a hollow stem)”. E.g. b: P N Linear equivalent would be: [a:N; b:{7,1,3,24} | ab]

Some Basic Z-Schema Examples (2/2): 

Some Basic Z-Schema Examples (2/2) Is equivalent to… Or linearly…

Naming Schemas: 

Naming Schemas MonCondition Or…

Z-Schema Decorations: 

Z-Schema Decorations Please refer to R. Pressman or other main-stream Software Engineering textbook.

Z-Schema Conventions: 

Z-Schema Conventions Delta Denoted by the Greek literal () Used to extend the schema components to indicate update operations, i.e. changes in state variables (updating operations). “Xi” Denoted by the Greek literal () Used to indicate that stored data is not affected, i.e. enquiry operations.

Delta Convention Examples(taken from Ince): 

Delta Convention Examples (taken from Ince) Specify a system which will keep track of students who have handed in Assignments. There are clearly three sets involved… Class (all the students in the class) HandedIn (all the students in the class who have handed in their assignment) NotHandedIn (all the students in the class who have not handed in their assignment)  Assignment

Use of a Delta Schema (based on previous example): 

Use of a Delta Schema (based on previous example) HandIn Model the handing in of a student assignment:

Use of a “Xi” Schema (based on previous example): 

Use of a “Xi” Schema (based on previous example)  Assignment Model a query for the number of students who have handed in: Therefore:

Schema Inclusion: 

Schema Inclusion A simple example of this will be presented during lectures.

Another Schema Inclusion Example (1/2): 

Another Schema Inclusion Example (1/2) FileStatus UserStatus

Another Schema Inclusion Example (2/2): 

Another Schema Inclusion Example (2/2) FileAndUserStatus Results in the following schema…

Another Schema Inclusion Example (taken from Ince): 

Another Schema Inclusion Example (taken from Ince) SetInv MidInv The above schemas result in… MidInv

Practical Z-Spec Example (elevator) (taken from Ghezzi): 

Practical Z-Spec Example (elevator) (taken from Ghezzi) This example is produced as a separate MS-Word document offered as a separate hand-out which should be circulated with this material.

Sequences: 

Sequences Are not sets Can be viewed as collections with predefined constraints Exist in different forms Can have operations applied to them Widespread use in computer systems

Types of Sequences: 

Types of Sequences Normal (including empty) seq Non-empty seq1 Injective (not containing duplicates) iseq Therefore…

Formal Sequence Definitions: 

Formal Sequence Definitions Definitions… seq T = = { f : N T | dom f = 1 .. #f } seq1 T = = { f : seq T | #f > 0 } iseq T = = seq T  (N T ) Some examples… E.g. of (seq N) is {13,29,3 9,4 11} written as 3,9,9,11 E.g. of (iseq files) is {1UpdateFile,2LogFile,3TaxFile} written as UpdateFile,LogFile,TaxFile

Sequences in Z: 

Sequences in Z Examples of these will be presented during lectures.

Sequence (in Z) Example: 

Sequence (in Z) Example FileQueue InQueue, OutQueue : seq Files #InQueue < #OutQueue Rentals Pending, Overdue : seq ID MostOverdue!, SoonToBeOverdue! : ID MostOverdue! = head Overdue SoonToBeOverdue! = head Pending

Tippruvawa din?: 

Tippruvawa din? Can you try to formally define the “head”, “last”, “tail”, and “front” sequence operators using a Z-schema?