csa2070 Formal slides

Information about csa2070 Formal slides

Published on November 16, 2007

Author: Maitane

Source: authorstream.com

Content

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?

Related presentations


Other presentations created by Maitane

Introduction DFT
16. 10. 2007
0 views

Introduction DFT

ch04 org cell
08. 05. 2008
0 views

ch04 org cell

taylor forcefeedback
08. 05. 2008
0 views

taylor forcefeedback

lecture01
07. 05. 2008
0 views

lecture01

majumdar iccs05
02. 05. 2008
0 views

majumdar iccs05

accident causation
02. 05. 2008
0 views

accident causation

452 lecture9
02. 05. 2008
0 views

452 lecture9

JohnAdamCAS
02. 05. 2008
0 views

JohnAdamCAS

v1exploratorium
02. 05. 2008
0 views

v1exploratorium

Ode to a rat
03. 10. 2007
0 views

Ode to a rat

crocodile physics
11. 10. 2007
0 views

crocodile physics

Critical Thinking
12. 10. 2007
0 views

Critical Thinking

Lectures 2
16. 10. 2007
0 views

Lectures 2

USLA
22. 10. 2007
0 views

USLA

Typologie etudiants 2005 2006
24. 10. 2007
0 views

Typologie etudiants 2005 2006

Land Ho The Isthmus Forms
25. 10. 2007
0 views

Land Ho The Isthmus Forms

Nobelpreis 2004
15. 10. 2007
0 views

Nobelpreis 2004

city sadness
01. 11. 2007
0 views

city sadness

ast110 02
13. 11. 2007
0 views

ast110 02

Mura
15. 10. 2007
0 views

Mura

INECOR Amar RACHEDI
24. 10. 2007
0 views

INECOR Amar RACHEDI

Intro RED Presentation
24. 10. 2007
0 views

Intro RED Presentation

MarseilleImprimable
24. 10. 2007
0 views

MarseilleImprimable

EOT Presentation
02. 11. 2007
0 views

EOT Presentation

OM 2005 11
16. 11. 2007
0 views

OM 2005 11

AdCooperate
11. 10. 2007
0 views

AdCooperate

CAPTIC2003 SV
23. 10. 2007
0 views

CAPTIC2003 SV

HPS PDS Yu 7 15 2007
01. 01. 2008
0 views

HPS PDS Yu 7 15 2007

f06 wk10
04. 01. 2008
0 views

f06 wk10

69A Job Safety Analysis Bayne
07. 01. 2008
0 views

69A Job Safety Analysis Bayne

Public Procurement Oct04 Notes
07. 01. 2008
0 views

Public Procurement Oct04 Notes

IST444Genomicsequenc ing
16. 10. 2007
0 views

IST444Genomicsequenc ing

informesept2006
22. 10. 2007
0 views

informesept2006

FunDgnCaseStudies2005
04. 10. 2007
0 views

FunDgnCaseStudies2005

SLP PP
22. 10. 2007
0 views

SLP PP

BinghamEtalWAFINAL
04. 12. 2007
0 views

BinghamEtalWAFINAL

ecoI 5
15. 10. 2007
0 views

ecoI 5

LIDAR Leblanc
19. 10. 2007
0 views

LIDAR Leblanc

orlando opening
29. 10. 2007
0 views

orlando opening

limestone
06. 12. 2007
0 views

limestone

212w
05. 10. 2007
0 views

212w

FPBASPSreport2006
04. 10. 2007
0 views

FPBASPSreport2006

PowerIndTrucksslides
27. 02. 2008
0 views

PowerIndTrucksslides

The Six Nutrients
04. 03. 2008
0 views

The Six Nutrients

fall trash
29. 02. 2008
0 views

fall trash

icfa korea may05
13. 03. 2008
0 views

icfa korea may05

traveling
03. 04. 2008
0 views

traveling

economic cycle
08. 04. 2008
0 views

economic cycle

LAH FADR 2007 01
21. 10. 2007
0 views

LAH FADR 2007 01

retrospective10year
09. 04. 2008
0 views

retrospective10year

telemonitor full
17. 04. 2008
0 views

telemonitor full

rules
22. 04. 2008
0 views

rules

History 101
23. 10. 2007
0 views

History 101

Agrofuels DrivingClimateChange
07. 04. 2008
0 views

Agrofuels DrivingClimateChange

cdc intervention
31. 10. 2007
0 views

cdc intervention

proj 05
28. 02. 2008
0 views

proj 05

appascom
01. 10. 2007
0 views

appascom

Ross7eCh11
16. 04. 2008
0 views

Ross7eCh11

Sato pres 06
19. 02. 2008
0 views

Sato pres 06

cvamia 2004
20. 02. 2008
0 views

cvamia 2004

QDS
20. 11. 2007
0 views

QDS

poster aises
26. 11. 2007
0 views

poster aises

CM1 NY Swipe Card presentation
28. 09. 2007
0 views

CM1 NY Swipe Card presentation

mississauga
05. 10. 2007
0 views

mississauga

RuralDevSeminar
18. 10. 2007
0 views

RuralDevSeminar

slides prog 65
30. 10. 2007
0 views

slides prog 65

SachsFelix
26. 02. 2008
0 views

SachsFelix

PSC300Week7Tue
23. 12. 2007
0 views

PSC300Week7Tue

Claus xpforedrag
06. 11. 2007
0 views

Claus xpforedrag

pre as18jan48
25. 03. 2008
0 views

pre as18jan48

RA2 conclusions 2
14. 02. 2008
0 views

RA2 conclusions 2