Course 02263
Formal Aspects of Software Engineering
RSL Maps
Anne E. Haxthausen DTU Compute
Technical University of Denmark aeha@dtu.dk
Contents
◆ what is a map
◆ map type expressions
◆ map value expressions
◆ map application
◆ map operators
◆ example of specification using maps
What is a Map?
A map (or table) is a collection of pairs of values.
Examples:
[′′
Klaus′′ 7→ 7,
′′John′′ 7→ 2,
′′Mary′′ 7→ 7 ]
[1 7→ 2, 5 7→ 10 ]
Maps may be:
◆ infinite
◆ partial
◆ non-deterministic on application
Map Type Expressions
◆ type_expr1 →m type_expr2 denotes the type consisting of map values [v1 7→ w1 , ..., vn 7→ wn ]
where n ≥ 0, vi : type_expr1, wi : type_expr2 and vi = vj ⇒ wi = wj May be partial: not all values in type_expr1 need to be in the domain.
Finite and deterministic when applied to elements vi in the domain.
◆ type_expr1 →m∼ type_expr2 denotes the type consisting of map values [v1 7→ w1 , ..., vn 7→ wn ],
[v1 7→ w1 , ..., vn 7→ wn, ...],
where n ≥ 0, vi : type_expr1, wi : type_expr2.
May be infinite and may be non-deterministic when applied to elements in the domain.
NB The original RSL book only has →m , but with the meaning of →m∼ .
Map Type Expressions, Examples
Nat →m Bool [ ]
[0 7→ true]
[0 7→ true, 1 7→ true ] ...
Nat →m∼ Bool [ ]
[0 7→ true]
[0 7→ true, 1 7→ true ] ...
[0 7→ true, 0 7→ false]
[0 7→ true, 1 7→ true, 2 7→ true, ...] ...
Map Value Expressions
Enumerated: [expr1 7→ expr1′,. . . ,exprn 7→ exprn′] [3 7→ true, 5 7→ false]
[′′
Klaus′′ 7→ 7, ′′John′′ 7→ 2, ′′Mary′′ 7→ 7]
Comprehended: [expr1 7→ expr2 | typing1,...,typingn • logical-expr3] [n 7→ 2∗n | n : Nat • n ≤ 2] = [0 7→ 0, 1 7→ 2, 2 7→ 4]
[n 7→ 2∗n | n : Nat ] = [0 7→ 0, 1 7→ 2, 2 7→ 4, ...]
Map Application
Basic form:
map-expr(expr1) Examples:
[′′
Klaus′′ 7→ 7, ′′John′′ 7→ 2, ′′Mary′′ 7→ 7](′′John′′) = 2 [3 7→ true, 3 7→ false](3) = true ⌈⌉ false
Application is always to values in the domain;
Associated Built-in Operators
dom : (T1 →m∼ T2) → T1-infset
rng : (T1 →m∼ T2) → T2-infset
† : (T1 →m∼ T2) × (T1 →m∼ T2) → (T1 →m∼ T2)
∪ : (T1 →m∼ T2) × (T1 →m∼ T2) → (T1 →m∼ T2)
dom [3 7→ true, 5 7→ false] = {3, 5}
dom [3 7→ true, 5 7→ false, 5 7→ true ] = {3, 5}
rng [3 7→ false, 5 7→ false] = {false} rng [3 7→ false, 5 7→ false, 5 7→ true] =
{false, true}
[3 7→ true, 5 7→ false] † [5 7→ true] = [3 7→ true, 5 7→ true]
[3 7→ true, 5 7→ false] ∪ [5 7→ true]
= [3 7→ true, 5 7→ false, 5 7→ true ]
\ : (T1 →m∼ T2) × T1-infset → (T1 →m∼ T2)
/ : (T1 ∼
→m T2) × T1-infset → (T1 →m∼ T2)
◦ : (T2 →m∼ T3) × (T1 →m∼ T2) → (T1 →m∼ T3)
∈ : T1 × (T1 →m∼ T2) → Bool
m \ s =
[d 7→ m(d) | d : T1 • d ∈ dom m ∧ d 6∈ s] [3 7→ true, 5 7→ false] \ {5, 7} = [3 7→ true] m / s =
[d 7→ m(d) | d : T1 • d ∈ dom m ∧ d ∈ s] [3 7→ true, 5 7→ false] / {5, 7} = [5 7→ false] m1 ◦ m2 =
[x 7→ m1(m2(x)) | x : T1 •
x ∈ dom m2 ∧ m2(x) ∈ dom m1 ] [3 7→ true, 5 7→ false] ◦
[′′
Klaus′′ 7→ 3, ′′John′′ 7→ 7]
= [′′
Klaus′′ 7→ true] 3 ∈ [3 7→ ′′
Anne′′] = true
NB the ∈ operator above was added to RSL after the book was written.
Example 1: Database Representations
type Database empty
insert(k1, d1, insert(k2,d2,empty)) type Database = (Key × Data)-set
{}
{(k1,d1), (k2,d2)}
type Database = (Key × Data)∗ hi
h(k1,d1), (k2,d2)i
type Database = Key →m Data [ ]
[k1 7→ d1, k2 7→ d2 ]
Example 1: Database
scheme MAP_DATABASE = class
type
Database = Key →m Data, Key, Data
value
empty : Database = [ ],
insert : Key × Data × Database → Database insert(k,d,db) ≡ db † [k 7→ d],
remove : Key × Database → Database remove(k,db) ≡ db \ {k},
defined : Key × Database → Bool defined(k,db) ≡ k ∈ dom db,
lookup : Key × Database →∼ Data lookup(k,db) ≡ db(k)
Example 2: Equivalence Relation (re-visited)
Example 2: Equivalence Relation (re-visited)
Example 2: Equivalence Relation (re-visited)
Example 2: Equivalence Relation (re-visited)
Example 2: Equivalence Relation (re-visited)
Example 2: Equivalence Relation
scheme EQUIVALENCE_RELATION = class
type
Elem, Partition_Id,
Relation = Elem →m∼ Partition_Id value
is_wf_Relation : Relation → Bool is_wf_Relation(r) ≡
(∀ e : Elem • e ∈ dom r ∧ (∃! p : Partition_Id • r(e) ≡ p)), are_equivalent : Elem × Elem × Relation →∼ Bool
are_equivalent(e1, e2, r) ≡ r(e1) = r(e2) pre {e1,e2} ⊆ dom r
... see next page end
Example 2: Equivalence Relation – Continued
value
initial : Relation axiom
is_wf_Relation(initial),
∀ e1, e2 : Elem • e1 6= e2 ⇒ initial(e1) 6= initial(e2) value
make_equivalent : Elem × Elem × Relation →∼ Relation make_equivalent(e1, e2, r) ≡
r † [e 7→ r(e2) | e : Elem • r(e) = r(e1) ] pre {e1,e2} ⊆ dom r
Example 3
Example 3
scheme BILL_OF_PRODUCTS = class
type
Product,
Bop = Product →m Product-set value
is_wf_Bop : Bop → Bool is_wf_Bop(bop) ≡
(∀ ps : Product-set • ps ∈ rng bop ⇒ ps ⊆ dom bop) ∧
(∀ p : Product • p ∈ dom bop ⇒ p 6∈ 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)} pre p ∈ dom bop,
depends_on : Product × Product × Bop →∼ Bool,
Example 3 — Continued
empty : Bop = [ ],
enter : Product × Product-set × Bop →∼ Bop - - enter a new product p enter(p,ps,bop) ≡ bop ∪ [p 7→ ps]
pre p 6∈ dom bop ∧ ps ⊆ dom bop,
add : Product × Product × Bop →∼ Bop - - add p2 as subproduct for p1 add(p1,p2,bop) ≡ bop † [p1 7→ bop(p1) ∪ {p2}]
pre
{p1,p2} ⊆ dom bop ∧ p1 6= p2 ∧ p2 6∈ bop(p1) ∧ p1 6∈ sub_products(p2,bop),
erase : Product × Product × Bop →∼ Bop - - remove p2 as subproduct for p1 erase(p1,p2,bop) ≡ bop † [p1 7→ bop(p1)\{p2} ]
pre p1 ∈ dom bop ∧ p2 ∈ bop(p1),
delete : Product × Bop →∼ Bop - - remove product p delete(p,bop) ≡ bop\{p}
pre p ∈ dom bop ∧
Example 3 - Home Exercise
1. How can bop1 from the example figure on one of the previous slides be created using the given functions?
2. The company introduces a new product p6 and p5 should have p6 as subproduct. How can you from bop1 create a new bop (using the
given functions) representing the new situation?
3. Now p4 should not anymore be a product supported by the company and in particular it should not be used as a subproduct for p2 and p3. How can you from the bop from the previous question create a new bop (using the given functions) representing the new situation?
