After studying this chapter you will be able to understand: Defining a type partial operators, basic types, type constructors, the set type constructor, operators on sets, operators on sets selecting elements, refinement. | Formal Methods in SE Lecture 21 VDM II Qaisar Javaid, Assistant Professor 2 1 3 Defining a type Partial Operators An operator op : T1 * . . . * Tn -> R is said to be total if, for any a1:T1,. . . an:Tn, the expression op(a1,. . ., an) is defined. If there exists some b1:T1,. . .,bn:Tn for which op(b1,. . .,bn) is undefined, op is said to be a partial operator. We avoid applying partial operators to values on which they are undefined! 4 Basic Types Type Symbol nat nat1 int real char Bool quote Values Natural numbers nat excluding 0 Integers Real Numbers Characters Booleans Named quote values Example Values 0, 1, 2, 1, 2, 3, ,-1,0,1,2, ‘g’, ‘@’ true, false , Operators +,-,*,/, +,-,*,/, +,-,*,/, +,-,*,/, =, and, or, =, 5 Type Constructors | Union types [_] Optional types :: Record types set of _ Finite sets seq of _ Finite sequences map _ to _ Finite mappings 6 The set type constructor The finite set type constructor is: set of _ What are the types of the following expressions? {1, -3, 12} { {9, 13, 77}, {32, 8}, {}, {77} } 7 The set type constructor The type set of X is the class of all possible finite sets of values drawn from the type X. For example: set of nat1 sets of non-zero Natural numbers set of Student sets of student records set of (seq of char) sets of sequences of characters (. sets of names) set of (set of int) sets of sets of integers, . { {3,56,2},{-2},{},{-33,5} } 8 Defining sets . (1) Enumeration: (2) Subrange (integers only): {integer1,.,integer2} . {12,.,20} = {12,.,12} = {9,.,3} = (0) Empty Set: {} 9 Defining sets . (3) Comprehension { expression | binding & predicate } The set of values of the expression under each assignment of values to bound variables satisfying the predicate. Consider all the values that can be taken by the variables in the binding. Restrict this to just those combinations of values which satisfy the predicate. Evaluate the expression for each combination. This gives . | Formal Methods in SE Lecture 21 VDM II Qaisar Javaid, Assistant Professor 2 1 3 Defining a type Partial Operators An operator op : T1 * . . . * Tn -> R is said to be total if, for any a1:T1,. . . an:Tn, the expression op(a1,. . ., an) is defined. If there exists some b1:T1,. . .,bn:Tn for which op(b1,. . .,bn) is undefined, op is said to be a partial operator. We avoid applying partial operators to values on which they are undefined! 4 Basic Types Type Symbol nat nat1 int real char Bool quote Values Natural numbers nat excluding 0 Integers Real Numbers Characters Booleans Named quote values Example Values 0, 1, 2, 1, 2, 3, ,-1,0,1,2, ‘g’, ‘@’ true, false , Operators +,-,*,/, +,-,*,/, +,-,*,/, +,-,*,/, =, and, or, =, 5 Type Constructors | Union types [_] Optional types :: Record types set of _ Finite sets seq of _ Finite sequences map _ to _ Finite mappings 6 The set type constructor The finite set type constructor is: set of _ What are the types of
