1- (*
2- * CLASS -+- TYPE --- RECORD --- CONNECTOR
3- * |
4- * +- BLOCK --- FUNCTION
5- * |
6- * +- PACKAGE
7- * |
8- * +- MODEL
9- *
10- *)
11-
1+ (**
2+ ** file: ClassInf.rml
3+ **
4+ ** This file deals with class inference, that is determining if a
5+ ** class definition adhers to one of the class restrictions, and, if
6+ ** specifically declared in a restrictied form, if it breaks that
7+ ** restriction.
8+ **
9+ ** The inference is implemented as a finite state machine. The
10+ ** relation `start' initializes a new machine, and the relation
11+ ** `trans' signals transitions in the machine. Finally, the state
12+ ** can be checked agains a restriction with the `valid' relation.
13+ **
14+ ** The restricted forms are ordered in a hierarchal fashion as
15+ ** described by the following diagram:
16+ **
17+ ** CLASS -+- TYPE --- RECORD --- CONNECTOR
18+ ** |
19+ ** +- BLOCK --- FUNCTION
20+ ** |
21+ ** +- PACKAGE
22+ ** |
23+ ** +- MODEL
24+ **
25+ **)
1226
1327module ClassInf :
1428
@@ -40,18 +54,30 @@ module ClassInf :
4054 | TYPE_STRING of string
4155 | TYPE_BOOL of string
4256
43- datatype Event = FOUND_EQUATION (* There are definitions *)
57+ (** The `Event' type contains the different events during *)
58+ (** instantiation that signals a possible machine transition. *)
59+ datatype Event = FOUND_EQUATION (* There are definitions inside *)
60+ (* the current definition *)
4461 | NEWDEF (* This is not a derived class *)
4562
46- relation print_restr : Restriction => ()
47- relation print_state : State => ()
4863 relation start : (Restriction, string) => State
4964 relation trans : (State, Event) => State
65+
5066 relation valid : (State, Restriction) => ()
67+ (* `assert_valid' is identical to 'valid'. The only difference is *)
68+ (* that it prints an error message when it fails. *)
5169 relation assert_valid : (State, Restriction) => ()
5270
71+ (* Debug relation *)
72+ relation print_restr : Restriction => ()
73+ relation print_state : State => ()
74+
5375end
5476
77+ (** relation: print_restr
78+ ** purpose: Output for debugging and error messages
79+ **)
80+
5581relation print_restr : Restriction => () =
5682
5783 rule print "CLASS"
@@ -104,6 +130,10 @@ relation print_restr : Restriction => () =
104130
105131end
106132
133+ (** relation: print_state
134+ ** purpose: Output for debugging and error messages
135+ **)
136+
107137relation print_state : State => () =
108138
109139 rule print "UNKNOWN " & print s
@@ -164,6 +194,10 @@ relation print_state : State => () =
164194
165195end
166196
197+ (** relation: start
198+ ** purpose: State machine initialization
199+ **)
200+
167201relation start : (Restriction, string) => State =
168202
169203 axiom start (R_CLASS, s) => UNKNOWN(s)
@@ -181,6 +215,9 @@ relation start : (Restriction, string) => State =
181215
182216end
183217
218+ (** relation: trans
219+ **)
220+
184221relation trans : (State, Event) => State =
185222
186223 (* NEWDEF *)
@@ -232,6 +269,9 @@ relation trans : (State, Event) => State =
232269
233270end
234271
272+ (** relation: valid
273+ **)
274+
235275relation valid : (State, Restriction) => () =
236276
237277 axiom valid(UNKNOWN(s), _)
@@ -266,6 +306,9 @@ relation valid : (State, Restriction) => () =
266306
267307end
268308
309+ (** relation: assert_valid
310+ **)
311+
269312relation assert_valid : (State, Restriction) => () =
270313
271314 rule valid(st,re)
0 commit comments