Course 02263
Formal Aspects of Software Engineering RSL Products and Bindings
Anne E. Haxthausen DTU Informatics (IMM) Technical University of Denmark
ah@imm.dtu.dk
Anne E. Haxthausen, Spring 2011c 02263 OH3 – p. 1/12
Contents
◆ what is a product? 3
◆ product type expressions 4
◆ product operators 4
◆ product value expressions 6
◆ examples of modeling using products 7
◆ binding and typings 11
c
Anne E. Haxthausen, Spring 2011 02263 OH3 – p. 2/12
What is a product?
Aproductis an ordered finite collection of values of possibly different types.
Examples:
(1,2)
(1,true,′′John′′)
Anne E. Haxthausen, Spring 2011c 02263 OH3 – p. 3/12
Product Type Expressions
type_expr1×. . . ×type_exprn, n≥2 denotes the type consisting of all values
(v1,. . . ,vn), where vi: type_expri Operators:
= 6=
c
Anne E. Haxthausen, Spring 2011 02263 OH3 – p. 4/12
Product Type Expessions, Examples
Bool×Bool
denotes the type consisting of the values:
(true,true) (true,false) (false,true) (false,false)
Nat×Nat×Bool
denotes the type consisting of the values:
(0,0,true) (0,0,false) (0,1,true) (0,1,false) (1,0,true) (1,0,false) (2,0,true)
...
Anne E. Haxthausen, Spring 2011c 02263 OH3 – p. 5/12
Product Value Expressions
(value_expr1,. . . ,value_exprn), n≥2 syntax semantics
e1 v1
... ...
en vn
(e1,. . . ,en) (v1,. . . ,vn) Examples:
(true∨false, 7 + 2) represents (true, 9)
c
Anne E. Haxthausen, Spring 2011 02263 OH3 – p. 6/12
Example: A System of Coordinates I
scheme SYSTEM_OF_COORDINATES= class
type
Position=Real×Real value
origin : Position=(0.0,0.0),
distance : Position×Position→Real distance((x1,y1),(x2,y2))≡
((x2−x1)↑2.0+(y2−y1)↑2.0)↑0.5 end
Anne E. Haxthausen, Spring 2011c 02263 OH3 – p. 7/12
Test Cases
scheme TEST_SYSTEM_OF_COORDINATES= extend SYSTEM_OF_COORDINATES with class
value
pos1 : Position=(1.0,1.0), pos2 : Position=(1.0,5.0), pos3 : Position=(5.0,1.0) test case
[t1] distance(origin, origin)=0.0, [t2] distance(pos1, pos2)=4.0, [t3] distance(pos1, pos3)=4.0, [t4] distance(pos1, origin) end
Translate to SML and run gives:
[t1] true [t2] true [t3] true
[t4] 1.41421356237
c
Anne E. Haxthausen, Spring 2011 02263 OH3 – p. 8/12
Example: A System of Coordinates II
scheme SYSTEM_OF_COORDINATES= class
type
Position=Real×Real value
origin : Position=(0.0,0.0),
distance : Position×Position→Real distance(p1,p2)≡
let
(x1,y1) = p1, (x2,y2) = p2 in
((x2−x1)↑2.0+(y2−y1)↑2.0)↑0.5 end
end
Anne E. Haxthausen, Spring 2011c 02263 OH3 – p. 9/12
(Explicit) Let Expressions
let
binding1= expr1, ...
bindingn= exprn in
expr end
c
Anne E. Haxthausen, Spring 2011 02263 OH3 – p. 10/12
Bindings
Examples:
x (x,y) (x,y,z)
((x1,y1),(x2,y2)) (x,(y,z))
Forms:
id
(binding1, ... , bindingn) Use:
◆ typings
◆ let expressions
◆ formal function parameters
◆ ...
Anne E. Haxthausen, Spring 2011c 02263 OH3 – p. 11/12
Typings
Examples:
x : Real (x,y) : Position a, b : Real Basic Form:
binding : type_expr Context condition:
binding must match type_expr Derived form:
binding1, ... , bindingn: type_expr Use:
◆ value definitions (e.g. value x : Real)
◆ quantified expressions (e.g.∀x : Real•x = x)
◆ ...
c
Anne E. Haxthausen, Spring 2011 02263 OH3 – p. 12/12
