- @Begin
- @Interface: ...
- @Commit_point_set:
- IDENTIFIER | IDENTIFIER ...
- @Condition: ... (Optional)
- @HB_Condition:
- IDENTIFIER :: <C_CPP_Condition>
- @HB_Condition: ...
- @ID: ... (Optional, use default ID)
- @Check: (Optional)
- ...
- @Action: (Optional)
- ...
- @Post_action: (Optional)
- @Post_check: (Optional)
- @End
-
- c) Potential commit construct
- @Begin
- @Potential_commit_point_define: ...
- @Label: ...
- @End
-
- d) Commit point define construct
- @Begin
- @Commit_point_define_check: ...
- @Label: ...
- @End
-
- OR
-
- @Begin
- @Commit_point_define: ...
- @Potential_commit_point_label: ...
- @Label: ...
- @End
-
- e) Entry point construct
- @Begin
- @Entry_point
- @End
-
- f) Interface define construct
- @Begin
- @Interface_define: <Interface_Name>
- @End
+ @Interface: InterfaceName // Required; a label to represent the interface
+ @LocalState: // Optional; to calculate the accumulative local state before this
+ // method call in a customized fashion. If not specified here, the
+ // local state would be default, which is the result of the
+ // execution on the subset of method calls in the sequential order
+ @PreCondition: // Optional; checking code
+ @LocalSideEffect: // Optional; to calculate the side effect this method call
+ // have on the local state in a customized fashion. If this
+ // field is not stated, it means we don't care about it.
+ @SideEffect: // Optional; to calculate the side effect on the global state. When
+ // the "@LocalSideEffect" specification is ommitted, we also impose the
+ // same side effect on the set of method calls that happen before this
+ // method call in the sequential order.
+ @PostCondition: // Optional; checking code
+
+
+ c) Ordering point construct
+ @OPDefine: condition // If the specified condition satisfied, the atomic
+ // operation right before is an ordering point
+
+ @PotentialOP(Label): condition // If the specified condition satisfied, the
+ // atomic operation right before is a potential
+ // ordering point, and we label it with a tag
+
+ @OPCheck(Label): condition // If the specified condition satisfied, the
+ // potential ordering point defined earlier with the
+ // same tag becomes an ordering point
+
+ @OPClear: condition // If the specified condition satisfied, all the
+ // ordering points and potential ordering points will be
+ // cleared
+
+ @OPClearDefine: condition // If the specified condition satisfied, all the
+ // ordering points and potential ordering points will
+ // be cleared, and the atomic operation right before
+ // becomes an ordering point. This is a syntax sugar
+ // as the combination of an "OPClear" and "OPDefine"
+ // statement
+