24 Semantics of
Let be the “meaning” function from to (set of
Boolean values, ) and let be an interval then
Let denote that the intervals and are identical with the possible exception
of the mapping for the variable .
Example 19 Let and be intervals.
The semantics of is defined in terms of
The semantics of ‘chop’ is as follows
Interval is a fusion of two intervals (satisfies ) and (satisfies
). State is shared by both.
Interval is infinite and satisfies , so is irrelevant.
The semantics of ‘chopstar’ is as follows
Finite interval is the fusion of a finite number of finite sub-intervals each satisfying
Infinite interval is the fusion of a finite number of sub-intervals each satisfying . Each
sub-interval is finite except the last one which is infinite.
Infinite interval is the fusion of an infinite number of finite sub-intervals each satisfying