Data Modelling Anne E. Haxthausen DTU Compute Technical University of Denmark aeha@dtu.dk

(1)

Course 02263

Formal Aspects of Software Engineering Data Modelling

Anne E. Haxthausen DTU Compute

Technical University of Denmark aeha@dtu.dk

c

�Anne E. Haxthausen, 2020 02263 OH9 – p. 1/28

Summary of RSL Type Deﬁnitions

You have learnt about two kinds of type deﬁnitions:

◆ sort deﬁnitions(typeid)

which declare names ofabstracttypes

◆ abbreviation deﬁnitions(typeid = type_expr) which (usually) give names toconcretetypes Later in this semester you will learn about:

◆ short record deﬁnitions(a la records in programming languages)

◆ union and variant type deﬁnitions(a la ML’s datatype declarations) including

■ enumeration type deﬁnitions typeid == v1|. . .|vn

■ option type deﬁnitions

typeoptT == none|some(valof : T)

c

Summary of RSL concrete data types

◆ basic types (Bool,Nat,Int,Real,Char,Text,Unit)

◆ composite types

■ products (T1×T2)

■ functions (T1→T2, T1→^∼ T2)

■ sets (T-set, T-infset)

■ lists (T^∗, T^ω)

■ maps (T1 →m T2, T1 →m^∼ T2)

◆ subtypes of concrete types

c

(2)

Short Records Example

Declaration of a record type named Book:

type Book ::

title : Title author : Author publisher : Publisher

Construction of values of typeBook:

mk_Book(t, a, p), where t : Title, a : Author, p : Publisher Field extraction from aBookvalueb:

title(b) author(b) publisher(b)

c

Short Records

Declaration of a record type named id:

type id ::

ﬁeld₁: type_expr₁ ...

ﬁeld_n: type_expr_n

Construction of values of type id:

mk_id(v₁,..., v_n), where v_i: type_expr_i Field extraction from a value v : id:

ﬁeld_i(v)

c

Short Records versus Products

Type deﬁnitions:

1.typeid ::ﬁeld₁: type_expr₁...ﬁeld_n: type_expr_n 2.typeid=type_expr₁×...×type_expr_n

Construction of values of type id:

1. mk_id(v₁,..., v_n), where v_i: type_expr_i 2. (v₁,..., v_n), where v_i: type_expr_i Field extraction from a value v : id:

1.ﬁeld_i(v)

2.let(v₁,..., v_n)=vinv_iend

c

Model-oriented vs Property-oriented Speciﬁcation Styles

Characterization:

◆ algebraic/property-oriented:

(main) types areabstract,

typically declared assortsand implicitly speciﬁed by declared values and axioms.

Example: typeDatabase

◆ model-oriented:

(main) types areconcretetypes that are constructed explicitly, typically from basic types and type constructors inabbreviation deﬁnitions.

Example: typeDatabase = Person-set Pragmatics:

◆ algebraic/property-oriented:

normally used in early development phases

◆ model-oriented:

normally used in later development phases

In this lecture we will give examples of model-oriented speciﬁcations.

c

(3)

Example: Bill of Materials

Exercise 9.4

◆ Revise the original speciﬁcation: For each product in a bop, the system should keep track of the number of occurrences of subproducts.

◆ Deﬁne a function making parts explosion.

c

Bill of Materials - Original Representation

c

Bill of Materials - Revised Representation

c

Original speciﬁcation

schemeBILL_OF_PRODUCTS= class

type Product,

Bop=Product →^m Product-set value

is_wf_Bop : Bop→Bool is_wf_Bop(bop)≡

(∀ps : Product-set^•ps∈rngbop⇒ps⊆dombop)∧ (∀p : Product^•p∈dombop⇒p6∈sub_products(p,bop)), sub_products : Product×Bop→^∼ Product-infset

sub_products(p,bop)≡

{p_sub|p_sub : Product^•depends_on(p,p_sub,bop)}

prep∈dombop,

depends_on : Product×Product×Bop→^∼ Bool, depends_on(p1,p2,bop)≡

p2∈bop(p1)∨

(∃p : Product^•(p∈bop(p1)∧depends_on(p,p2,bop))) prep1∈dombop

c

(4)

Original Speciﬁcation — Continued

empty : Bop=[ ],

enter : Product×Product-set×Bop→^∼ Bop enter(p,ps,bop)≡bop∪[p7→ps]

prep6∈dombop∧ps⊆dombop, delete : Product×Bop→^∼ Bop delete(p,bop)≡bop\{p}

prep∈dombop∧

∼(∃ps : Product-set^•ps∈rngbop∧p∈ps), add : Product×Product×Bop→^∼ Bop

add(p1,p2,bop)≡bop†[p17→bop(p1)∪{p2}] pre

{p1,p2}⊆dombop∧p16=p2∧p26∈bop(p1)∧

p16∈sub_products(p2,bop),

erase : Product×Product×Bop→^∼ Bop erase(p1,p2,bop)≡bop†[p17→bop(p1)\{p2}] prep1∈dombop∧p2∈bop(p1)

end

c

Revised speciﬁcation

schemeBILL_OF_PRODUCTS= class

type Product,

Bop={|bop : Bop′_•is_wf_Bop(bop)|}, Bop′

=Product →^m Table,

Table=Product →^m N1, N1={|n :Nat^•n≥1|}

value

is_wf_Bop : Bop′

→Bool is_wf_Bop(bop′)≡

(∀t : Table^•t∈rngbop′

⇒domt⊆dombop′)∧ (∀p : Product^•p∈dombop′

⇒p6∈sub_products(p, bop′)), sub_products : Product×Bop′ ∼

→Product-infset sub_products(p, bop′)≡

{p_sub|p_sub : Product^•depends_on(p, p_sub, bop′ )} prep∈dombop′,

depends_on : Product×Product×Bop′ ∼

→Bool depends_on(p1, p2, bop′)≡

p2∈dombop′ (p1)∨

(∃p : Product^•(p∈dombop′

(p1)∧depends_on(p, p2, bop′ ))) prep1∈dombop′

c ,

Revised speciﬁcation – continued

empty : Bop=[ ],

enter : Product×Table×Bop→^∼ Bop enter(p, t, bop)≡bop∪[p7→t] prep6∈dombop∧domt⊆dombop, delete : Product×Bop→^∼ Bop

delete(p, bop)≡bop\ {p}

prep∈dombop∧ ∼(∃t : Table^•t∈rngbop∧p∈domt), add : Product×Product×N1×Bop→^∼ Bop

add(p1, p2, n, bop)≡bop†[p17→bop(p1)∪[p27→n] ] pre

{p1, p2}⊆dombop∧p16=p2∧p26∈dombop(p1)∧

p16∈sub_products(p2, bop),

erase : Product×Product×Bop→^∼ Bop

erase(p1, p2, bop)≡bop†[p17→bop(p1)\ {p2}] prep1∈dombop∧p2∈dombop(p1)

end

c

Parts-Explosion: aux. functions

schemeTABLE_OPERATIONS= extendBILL_OF_PRODUCTSwith

class value

+: Table×Table→Table t1+t2≡

[ p7→count(p, t1)+count(p, t2)| p : Product^•p∈domt1∪domt2 ],

∗: N1×Table→Table

n1∗t≡[ p7→n1∗t(p)|p : Product^•p∈domt ], count : Product×Table→Nat

count(p, t)≡ifp∈domtthent(p)else0end end

Example of function applications:

3∗[p47→4] = [p47→12],

5∗[p47→6, p57→9] = [p47→30, p57→45],

[p47→12] + [p47→30, p57→45] = [p47→42, p57→45]

c

(5)

Parts-explosion, expected results

valuep, p1, p2, p3, p4, p5 : Product valuebop1 : Bop=

[p 7→[p17→2, p27→3, p37→5], p17→[ ],

p27→[p47→4],

p37→[p47→6, p57→9], p47→[ ],

p57→[ ] ]

valueparts_of_product : Product×Bop→^∼ Table test case

parts_of_product(p1, bop)= [p17→1], parts_of_product(p2, bop)= [p47→4],

parts_of_product(p3, bop)= [p47→6, p57→9], parts_of_product(p4, bop)= [p47→1],

parts_of_product(p5, bop)= [p57→1],

parts_of_product( p, bop)= [p17→2, p47→3∗4+5∗6, p57→5∗9]

c

Parts-explosion, towards an algorithm

For atomic productsp:

parts_of_product(p, bop)≡[p7→1] For composite productsp:

parts_of_product(p, bop)≡parts_of_table(bop(p), bop) For tables:

parts_of_table([p_17→n_1,..., p_N7→n_N], bop)≡ n_1∗parts_of_product(p_1, bop)+

...+

n_N∗parts_of_product(p_N, bop)

c

Parts-explosion

schemePARTS_EXPLOSION=

extendTABLE_OPERATIONSwith class value

parts_of_product : Product×Bop→^∼ Table parts_of_product(p, bop)≡

lett=bop(p)in

ift=[ ]then[p7→1] /∗p is atomic∗/

elseparts_of_table(bop(p), bop) /∗p is composite∗/

end end

prep∈dombop,

parts_of_table : Table×Bop→^∼ Table parts_of_table(t, bop)≡

ift=[ ]then[ ]

else letp : Product^•p∈domtin t(p)∗parts_of_product(p, bop)+ parts_of_table(t\ {p}, bop) end end

pre domt⊆dombop end

c

Example: Bank System (Exercise 9.3)

Requirements

R1 Eachcustomerhas 0, 1 or moreaccounts.

R2 Anaccounthas abalance.

R3 Eachcustomerhas anoverdraft.

R4 Two distinctcustomers can’t share anaccount.

R5 Accounts must not be overdrawn (more than theoverdraft).

Question 1Deﬁne appropriate types!

Bank System Basic Types type

CuNo, AcNo,

Balance=Int, Overdraft=Nat

c

(6)

Bank Example

Requirements

R1 Eachcustomerhas 0, 1 or moreaccounts.

R2 Anaccounthas abalance.

R3 Eachcustomerhas anoverdraft.

R4 Two distinctcustomers can’t share anaccount.

R5 Accounts must not be overdrawn (more than theoverdraft).

Example of a Bank

c

Bank Models

typeBank1=(CuNo →^m Overdraft)×(CuNo →^m (AcNo →^m Balance)) typeBank2=CuNo →^m (Overdraft×(AcNo →^m Balance))

typeBank3=(CuNo →m Overdraft)×(AcNo →m (CuNo×Balance)) valueb1 : Bank1=

([Petersen7→500, Larsen7→0],

[Petersen7→[41017→10000, 41027→300, 41057→ −400], Larsen7→[41037→700, 41047→ 5]

])

valueb2 : Bank2=

[Petersen7→(500,[41017→10000, 41027→300, 41057→ −400]), Larsen 7→(0,[41037→700, 41047→ 5])

]

valueb3 : Bank3=

([Petersen7→500, Larsen7→0], [

41017→(Petersen, 10000), 41027→(Petersen, 300), 41037→(Larsen, 700), 41047→(Larsen, 5), 41057→(Petersen,−400) ]

)

c

Bank Model 1

typeBank1=(CuNo →^m Overdraft)×(CuNo →^m (AcNo →^m Balance)) valueb1 : Bank1=

([Petersen7→500, Larsen7→0],

[Petersen7→[41017→10000, 41027→300, 41057→ −400], Larsen7→[41037→700, 41047→ 5]

]) value

is_wff : Bank1→Bool is_wff(om, km)≡

domkm⊆domom ∧- - R3 (∀ cu1, cu2 : CuNo^•

{cu1, cu2}⊆domkm∧cu16=cu2⇒

domkm(cu1) ∩ domkm(cu2)={}

) - - R4

∧

(∀ cu : CuNo^•cu ∈ domkm⇒ (∀ ac : AcNo^•ac ∈ domkm(cu)⇒

km(cu)(ac)+om(cu)≥0) ) - - R5

c

Bank Model 2

type Bank2=CuNo →m (Overdraft×(AcNo →m Balance)) valueb2 : Bank2=

[Petersen7→(500,[41017→10000, 41027→300, 41057→ −400]), Larsen 7→(0,[41037→700, 41047→ 5])

] value

is_wff : Bank2→Bool is_wff(b) ≡

(∀ cu1, cu2 : CuNo^•

{cu1, cu2}⊆domb∧cu16=cu2⇒

let(o1, m1)=b(cu1), (o2, m2)=b(cu2)in domm1 ∩ domm2={}

end ) - - R4

∧

(∀ cu : CuNo^•cu ∈ domb⇒ let(o, m)=b(cu)in

∀ ac : AcNo^•ac ∈ domm⇒m(ac)+o≥0 end

) - - R5

c

(7)

Bank Model 3

typeBank3=(CuNo →^m Overdraft)×(AcNo →^m (CuNo×Balance)) valueb3 : Bank3=

([Petersen7→500, Larsen7→0], [

41017→(Petersen, 10000), 41027→(Petersen, 300), 41037→(Larsen, 700), 41047→(Larsen, 5), 41057→(Petersen,−400) ]

) value

is_wff : Bank3→Bool is_wff(om, m) ≡

(

∀ cu : CuNo, i : Balance^•(cu, i) ∈ rngm⇒ cu ∈ domom∧i+om(cu)≥0

) - - R3 and R5

c

A lesson

The more redundancy in the data types –

the more conditions are found in the is_wff functions

c

Bank System: Exercise 9.3, Question 2

Deﬁne the following functions:

◆ new_customer,

◆ new_account,

◆ balance,

◆ delete_customer,and

◆ delete_account for bank model 3.

c

Banking Functions

typeBank={|b : Bank3•is_wff(b)|},

Bank3=(CuNo →m Overdraft)×(AcNo →m (CuNo×Balance)) value

new_customer : CuNo×Overdraft×Bank→^∼Bank new_customer(cu, o, (om, m)) ≡ (om ∪ [cu7→o], m)

precu6∈ domom,

new_account : CuNo×AcNo×Bank→^∼Bank

new_account(cu, ac, (om, m)) ≡ (om, m ∪ [ac7→(cu, 0)]) precu ∈ domom∧ac6∈ domm,

balance : AcNo×Bank→^∼Balance

balance(ac, (om, m)) ≡ let(cu, i)=m(ac)iniend preac ∈ domm,

delete_account : AcNo×Bank→^∼Bank delete_account(ac, (om, m)) ≡ (om, m\ {ac})

preac∈domm,

delete_customer : CuNo×Bank→^∼Bank delete_customer(cu, (om, m)) ≡ (om\ {cu}, m)

precu∈domom∧(∀i : Balance•(cu, i)6∈rngm)

c