edits

diff --git a/notes/definition.cc b/notes/definition.cc
index bcc01e7b167702a6b062fcaa5d72770643b48b0c..0c5b7965174727e5414f005c0421f33188937e35 100644 (file)
--- a/notes/definition.cc
+++ b/notes/definition.cc
@@ -32,7 +32,7 @@ typedef set<int> IntSet;
 
 /********** More general specification-related types and operations **********/
 
 
 /********** More general specification-related types and operations **********/
 

-#define NewSet new set<Method>
+#define NewMethodSet new set<Method>

 
 #define CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */
 #define CAT_HELPER(a, b) a ## b
 
 #define CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */
 #define CAT_HELPER(a, b) a ## b


@@ -74,7 +74,7 @@ typedef set<int> IntSet;
 /*
 #define Subset(s, subset, condition) \
        MethodSet original = s; \
 /*
 #define Subset(s, subset, condition) \
        MethodSet original = s; \

-       MethodSet subset = NewSet; \
+       MethodSet subset = NewMethodSet; \

        ForEach (_M, original) { \
                if ((condition)) \
                        subset->insert(_M); \
        ForEach (_M, original) { \
                if ((condition)) \
                        subset->insert(_M); \


@@ -213,7 +213,7 @@ inline MethodSet MakeSet(int count, ...) {
        MethodSet res;
 
        va_start (ap, count);
        MethodSet res;
 
        va_start (ap, count);

-       res = NewSet;
+       res = NewMethodSet;

        for (int i = 0; i < count; i++) {
                Method item = va_arg (ap, Method);
                res->insert(item);
        for (int i = 0; i < count; i++) {
                Method item = va_arg (ap, Method);
                res->insert(item);


@@ -281,7 +281,7 @@ int main() {
        is2->insert(5);
 
 
        is2->insert(5);
 
 

-       MethodSet ms = NewSet;
+       MethodSet ms = NewMethodSet;

        Method m = new MethodCall;
        m->interfaceName = "Store";
        StateStruct *ss = new StateStruct;
        Method m = new MethodCall;
        m->interfaceName = "Store";
        StateStruct *ss = new StateStruct;

diff --git a/notes/nondeterm-spec.txt b/notes/nondeterm-spec.txt
index e594157979779034fb912193f232a76b9dc6926c..d1011dce5e81e83fddcc5eb1bdeb8d8fd810dedb 100644 (file)
--- a/notes/nondeterm-spec.txt
+++ b/notes/nondeterm-spec.txt
@@ -93,13 +93,113 @@ IV. Examples
 We define a struct called MethodCall to represent the data we would collect and
 communicate between the real execution and the checking process.
 
 We define a struct called MethodCall to represent the data we would collect and
 communicate between the real execution and the checking process.
 

+
+STATE(field)   // A primitive to access the current state in the interface
+                               // specification by the name of the field. We can use this as a
+                               // lvalue & rvalue ==> "STATE(x) = 1" and "int i = STATE(x)" are
+                               // both okay
+
+                               // This can also be used to refer to the state of a method item
+                               // in the Subset operation (see Subset)
+
+NAME                   // Used to refer to the name of a method item in the Subset
+                               // operation (see Subset)
+
+RET(type)              // Used to refer to the return value of a method item in the
+                               // Subset operation (see Subset)
+
+ARG(type, arg) // Used to refer to the argument of a method item in the
+                               // Subset operation (see Subset)
+
+
+PREV           // Represent the set of previous method calls of the current method
+                       // call
+
+CONCURRENT     // Represent the set of concurrent method calls of the current
+                               // method call
+
+NEXT           // Represent the set of next method calls of the current method
+                       // call
+
+Name(method)           // The interface label name of the specific method
+
+State(method, field)           // A primitive to access a specific state field of a
+                                                       // specific method. Also used as lvalue and rvalue
+
+Ret(method, type)              // The return value of the specific method; type should
+                                               // be the name of the interface label
+
+Arg(method, type, arg) // The arguement by name of the specific method; type should
+                                               // be the name of the interface label, and arg should be
+                                               // the name of the argument
+
+Prev(method)           // Represent the set of previous method calls of the
+                                       // specific method call
+
+Next(method)           // Represent the set of next method calls of the specific
+                                       // method call
+
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+ForEach(item, container) { ... }       // Useful iteration primitive
+
+NewMethodSet           // Create a new method set (set<MethodCall*>*)
+
+MakeSet(NewSetType, oldset, newset, field);            // 
+
+Subset(set, condition) // A generic subset operation that takes a condition and
+                                               // returns all the item for which the boolean guard
+                                               // holds. The condition can be specified with GUARD or
+                                               // GeneralGuard shown as follow.
+
+ITEM   // Used to refer to the set item in the GeneralGuard shown below
+
+GeneralGuard(type, expression) // Used as a condition for any set<T> type. We
+                                                               // use "ITEM" to refer to a set item. For
+                                                               // example, a subset of positive elements on an
+                                                               // IntSet "s" would be
+                                                               // "Subset(s, GeneralGuard(int, ITEM > 0))"
+
+Guard(expression)      // Used specifically for MethodSet(set<MethodCall*>). An
+                                       // example to extract the subset of method calls in the PREV
+                                       // set that is a "Store" method and whose state "x" is equal
+                                       // to "val" and the return value is 5 would be
+                                       // "Subset(PREV, Guard(STATE(x) == val && NAME == "Store" &&
+                                       // RET(Store) == 5))"
+
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+
+
+To make things easier, we have the following helper macros.
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+/**
+       This is a common macro that is used as a constant for the name of specific
+       variables. We basically have two usage scenario:
+       1. In Subset operation, we allow users to specify a condition to extract a
+       subset. In that condition expression, we provide NAME, RET(type), ARG(type,
+       field) and LOCAL(field) to access each item's (method call) information.
+       2. In general specification (in pre- & post- conditions and side effects),
+       we would automatically generate an assignment that assign the current
+       MethodCall* pointer to a variable namedd _M. With this, when we access the
+       local state of the current method, we use LOCAL(field) (this is a reference
+       for read/write).
+*/
+#define ITEM _M
+#define _M ME
+
+#define CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */
+#define CAT_HELPER(a, b) a ## b
+#define X(name) CAT(__##name, __LINE__) /* unique variable */
+
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+

 *****************************************************************************
 typedef struct MethodCall {
        string name; // The interface label name
        void *value; // The pointer that points to the struct that have the return
                                 // value and the arguments
        void *state; // The pointer that points to the struct that represents
 *****************************************************************************
 typedef struct MethodCall {
        string name; // The interface label name
        void *value; // The pointer that points to the struct that have the return
                                 // value and the arguments
        void *state; // The pointer that points to the struct that represents

-                                         // the (local) state
+                                         // the state

        set<MethodCall*> *prev; // Method calls that are hb right before me
        set<MethodCall*> *concurrent; // Method calls that are concurrent with me
        set<MethodCall*> *next; // Method calls that are hb right after me
        set<MethodCall*> *prev; // Method calls that are hb right before me
        set<MethodCall*> *concurrent; // Method calls that are concurrent with me
        set<MethodCall*> *next; // Method calls that are hb right after me