package C { abstract class CExpression { attribute needsBracket : boolean; attribute kind : String; attribute cexpId : String; attribute isStatic : boolean; reference type : CType; reference elementType : CType; operation newCBasicExpression(id : String , name : String , t : CType ) : CExpression pre: true post: CBasicExpression->exists( b | b.cexpId = id & b.data = name & b.kind = "variable" & b.type = t & b.elementType = t & result = b ); operation defineCOpRef(op : COperation ) : CExpression pre: true post: CBasicExpression->exists( be | be.cexpId = op.name + "_ref" & be.data = op.name & be.type = op.returnType & result = be ); operation defineCOpReference(op : String , typ : String ) : CExpression pre: true post: CBasicExpression->exists( be | be.cexpId = op + "_ref" & be.data = op & CPrimitiveType->exists( t | t.name = typ & t.ctypeId = op + "_" + typ & be.type = t & be.elementType = t & result = be ) ); operation toString() : String pre: true post: result = " "; } class CBinaryExpression extends CExpression { attribute operator : String; reference left : CExpression; reference right : CExpression; operation toString() : String pre: true post: ( needsBracket = true => result = "(" + left + " " + operator + " " + right + ")" ) & ( true => result = left + " " + operator + " " + right ); } class CUnaryExpression extends CExpression { attribute operator : String; reference argument : CExpression; operation toString() : String pre: true post: result = operator + argument; } abstract class CType { attribute ctypeId : String; attribute name : String; operation newCType(id : String , name : String ) : CType pre: true post: CPrimitiveType->exists( t | t.ctypeId = id & t.name = name & result = t ); } class CBasicExpression extends CExpression { attribute data : String; reference parameters[*] ordered : CExpression; reference arrayIndex[0-1] : CExpression; reference reference[0-1] : CExpression; operation parameterString(p : Sequence(CExpression) ) : String pre: true post: ( p.size = 0 => result = "" ) & ( p.size = 1 => result = "" + p[1] ) & ( p.size > 1 => result = p[1] + ", " + parameterString(p.tail) ); operation parString() : String pre: true post: ( parameters.size = 0 & kind = "operation" => result = "()" ) & ( parameters.size = 0 & kind /= "operation" => result = "" ) & ( parameters.size > 0 => result = "(" + parameterString(parameters) + ")" ); operation toString() : String pre: true post: ( arrayIndex.size = 0 & reference.size = 0 => result = data + parString() ) & ( arrayIndex.size > 0 & reference.size = 0 => result = data + "[" + arrayIndex.any + " -1]" ) & ( arrayIndex.size = 0 & reference.size > 0 => result = reference.any + "->" + data ) & ( arrayIndex.size > 0 & reference.size > 0 => result = reference.any + "->" + data + "[" + arrayIndex.any + " -1]" ); } class CPrimitiveType extends CType { attribute name identity : String; operation toString() : String pre: true post: result = name; } class CArrayType extends CType { attribute duplicates : boolean; reference componentType : CType; operation toString() : String pre: true post: result = componentType + "*"; } class CPointerType extends CType { reference pointsTo : CType; operation toString() : String pre: true post: result = pointsTo + "*"; } class CStruct extends CType { attribute name identity : String; reference members[*] ordered : CMember; reference allMembers[*] : CMember; operation toString() : String pre: true post: result = "struct " + name; operation allCMembers() : Set(CMember) pre: true post: sups = members->select(name = "super") & ( sups.size = 0 => result = members ) & ( sups.size > 0 => result = ( members - sups )->union(sups.any.inheritedCMembers()) ); operation createOp(ent : String ) : String pre: true post: einst = ent.toLowerCase + "_instances" & result = "struct " + ent + "* create" + ent + "(void)\n" + "{ struct " + ent + "* result = (struct " + ent + "*) malloc(sizeof(struct " + ent + "));\n" + members->collect( m | m.initialiser() )->sum() + " " + einst + " = append" + ent + "(" + einst + ", result);\n" + " " + ent.toLowerCase + "_size++;\n" + " return result;\n" + "}\n"; operation createPKOp(ent : String , key : String ) : String pre: true post: einst = ent.toLowerCase + "_instances" & result = "struct " + ent + "* create" + ent + "(char* _value)\n" + "{ struct " + ent + "* result = NULL;\n" + " result = get" + ent + "ByPK(_value);\n" + " if (result != NULL) { return result; }\n" + " result = (struct " + ent + "*) malloc(sizeof(struct " + ent + "));\n" + members->collect( m | m.initialiser() )->sum() + " set" + ent + "_" + key + "(result, _value);\n" + " " + einst + " = append" + ent + "(" + einst + ", result);\n" + " " + ent.toLowerCase + "_size++;\n" + " return result;\n" + "}\n"; operation concatenateOp() : String pre: true post: result = "struct " + name + "** concatenate" + name + "(struct " + name + "* _col1[], struct " + name + "* _col2[])\n" + "{ int _n = length((void**) _col1);\n" + " int _m = length((void**) _col2);\n" + " struct " + name + "** result = (struct " + name + "**) calloc(_n + _m + 1, sizeof(struct " + name + "*));\n" + " int i = 0;\n" + " int j = 0;\n" + " for ( ; i < _n; i++)\n" + " { result[j] = _col1[i];\n" + " j++;\n" + " }\n" + " i = 0;\n" + " for ( ; i < _m; i++)\n" + " { result[j] = _col2[i];\n" + " j++;\n" + " }\n" + " result[j] = NULL;\n" + " return result;\n" + "}\n"; operation intersectionOp() : String pre: true post: result = "struct " + name + "** intersection" + name + "(struct " + name + "* _col1[], struct " + name + "* _col2[])\n" + "{ int n = length((void**) _col1);\n" + " int m = length((void**) _col2);\n" + " struct " + name + "** result = (struct " + name + "**) calloc(n + 1, sizeof(struct " + name + "*));\n" + " int i = 0;\n" + " int j = 0;\n" + " for ( ; i < n; i++)\n" + " { struct " + name + "* _ex = _col1[i];\n" + " if (isIn((void*) _ex, (void**) _col2))\n" + " { result[j] = _ex; j++; }\n" + " }\n" + " result[j] = NULL;\n" + " return result;\n" + "}\n"; operation insertAtOp() : String pre: true post: result = "struct " + name + "** insertAt" + name + "(struct " + name + "* _col1[], int ind, struct " + name + "* _col2[])\n" + "{ if (ind <= 0) { return _col1; }\n" + " int n = length((void**) _col1);\n" + " int m = length((void**) _col2);\n" + " if (m == 0) { return _col1; }\n" + " struct " + name + "** result = (struct " + name + "**) calloc(n + m + 1, sizeof(struct " + name + "*));\n" + " int i = 0; int j = 0;\n" + " for ( ; i < ind - 1 && i < n; i++)\n" + " { result[i] = _col1[i]; }\n" + " if (i == ind - 1)\n" + " { for ( ; j < m; j++, i++)\n" + " { result[i] = _col2[j]; }\n" + " for ( ; i < n + m; i++)\n" + " { result[i] = _col1[i - m]; }\n" + " }\n" + " else \n" + " { for ( ; j < m; j++, i++)\n" + " { result[i] = _col2[j]; }\n" + " }\n" + " result[n+m] = NULL;\n" + " return result;\n" + "}\n"; operation exists1Op() : String pre: true post: result = "unsigned char exists1" + name + "(struct " + name + "* _col[], unsigned char (*test)(struct " + name + "*))\n" + "{ int n = length((void**) _col);\n" + " unsigned char result = FALSE; \n" + " unsigned char found = FALSE;\n" + " int i = 0; \n" + " for ( ; i < n; i++)\n" + " { struct " + name + "* ex = _col[i];\n" + " if (ex == NULL) { return result; }\n" + " if ((*test)(ex))\n" + " { if (found) { return FALSE; }\n" + " else { found = TRUE; }\n" + " }\n" + " }\n" + " if (found) { return TRUE; }\n" + " return result;\n" + "}\n"; operation isUniqueOp() : String pre: true post: result = "unsigned char isUnique" + name + "(struct " + name + "* _col[], void* (*fe)(struct " + name + "*))\n" + "{ unsigned char result = TRUE; \n" + " void** _values = collect" + name + "(_col, fe);\n" + " int n = length((void**) _values);\n" + " int i = 0; \n" + " for ( ; i < n; i++)\n" + " { void* ex = _values[i];\n" + " if (i < n - 1 && isIn(ex, _values + (i + 1)))\n" + " { return FALSE; }\n" + " }\n" + " return result;\n" + "}\n"; operation frontOp() : String pre: true post: result = "struct " + name + "** front" + name + "(struct " + name + "* _col[])\n" + "{ int n = length((void**) _col);\n" + " return subrange" + name + "(_col, 1, n-1); }\n"; operation tailOp() : String pre: true post: result = "struct " + name + "** tail" + name + "(struct " + name + "* _col[])\n" + "{ int n = length((void**) _col);\n" + " return subrange" + name + "(_col, 2, n); }\n"; operation collectPrimOp(t : String ) : String pre: true post: result = " " + t + "* collect" + name + "_" + t + "(struct " + name + "* _col[], " + t + " (*fe)(struct " + name + "*))\n" + " { int n = length((void**) _col);\n" + " " + t + "* result = (" + t + "*) calloc(n, sizeof(" + t + "));\n" + " int i = 0;\n" + " for ( ; i < n; i++)\n" + " { struct " + name + "* self = _col[i];\n" + " result[i] = (*fe)(self);\n" + " }\n" + " return result;\n" + " }\n"; operation removeAllOp() : String pre: true post: result = "struct " + name + "** removeAll" + name + "(struct " + name + "* _col1[], struct " + name + "* _col2[])\n" + "{ int n = length((void**) _col1);\n" + " struct " + name + "** result = (struct " + name + "**) calloc(n+1, sizeof(struct " + name + "*));\n" + " int i = 0; int j = 0;\n" + " for ( ; i < n; i++)\n" + " { struct " + name + "* ex = _col1[i];\n" + " if (isIn((void*) ex, (void**) _col2)) {}\n" + " else \n" + " { result[j] = ex; j++; }\n" + " }\n" + " result[j] = NULL;\n" + " return result;\n" + "}\n"; operation asSetOp() : String pre: true post: result = "struct " + name + "** asSet" + name + "(struct " + name + "* _col[])\n" + "{ int n = length((void**) _col);\n" + " if (n == 0) { return _col; }\n" + " struct " + name + "** result = (struct " + name + "**) calloc(n + 1, sizeof(struct " + name + "*));\n" + " int i = 0; int j = 0;\n" + " result[j] = NULL;\n" + " for ( ; i < n; i++)\n" + " { struct " + name + "* ex = _col[i];\n" + " if (isIn((void*) ex, (void**) result)) {}\n" + " else \n" + " { result[j] = _col[i]; j++;\n" + " result[j] = NULL; }\n" + " } \n" + " result[j] = NULL;\n" + " return result;\n" + "}\n"; } class CMember { attribute name : String; attribute isKey : boolean; reference type : CType; operation inheritedCMembers() : Set(CMember) pre: type : CPointerType & type.pointsTo : CStruct post: anc = type.pointsTo & result = anc.allCMembers(); operation getterOp(ent : String ) : String pre: true post: result = type + " get" + ent + "_" + name + "(struct " + ent + "* self) { return self->" + name + "; }\n"; operation inheritedGetterOp(ent : String , sup : String ) : String pre: true post: ( name /= "super" => result = type + " get" + ent + "_" + name + "(struct " + ent + "* self) { return get" + sup + "_" + name + "(self->super); }\n" ) & ( name = "super" => result = self.ancestorGetterOps(ent,sup) ); operation ancestorGetterOps(ent : String , sup : String ) : String pre: type : CPointerType & type.pointsTo : CStruct post: anc = type.pointsTo & result = anc.members->collect( m | m.inheritedGetterOp(ent,sup) )->sum(); operation inheritedGetterOps(ent : String ) : String pre: type : CPointerType & type.pointsTo : CStruct post: sup = type.pointsTo & result = sup.members->collect( m | m.inheritedGetterOp(ent,sup.name) )->sum(); operation setterOp(ent : String ) : String pre: true post: result = "void set" + ent + "_" + name + "(struct " + ent + "* self, " + type + " _value) { self->" + name + " = _value; }\n"; operation inheritedSetterOp(ent : String , sup : String ) : String pre: true post: ( name /= "super" => result = "void set" + ent + "_" + name + "(struct " + ent + "* self, " + type + " _value) { set" + sup + "_" + name + "(self->super, _value); }\n" ) & ( name = "super" => result = self.ancestorSetterOps(ent,sup) ); operation ancestorSetterOps(ent : String , sup : String ) : String pre: type : CPointerType & type.pointsTo : CStruct post: anc = type.pointsTo & result = anc.members->collect( m | m.inheritedSetterOp(ent,sup) )->sum(); operation inheritedSetterOps(ent : String ) : String pre: type : CPointerType & type.pointsTo : CStruct post: sup = type.pointsTo & result = sup.members->collect( m | m.inheritedSetterOp(ent,sup.name) )->sum(); operation getAllOp(ent : String ) : String pre: true post: result = type + "* getAll" + ent + "_" + name + "(struct " + ent + "* _col[])\n" + "{ int n = length((void**) _col);\n" + " " + type + "* result = (" + type + "*) calloc(n, sizeof(" + type + "));\n" + " int i = 0;\n" + " for ( ; i < n; i++)\n" + " { result[i] = get" + ent + "_" + name + "(_col[i]); }\n" + " return result;\n" + "}\n"; operation getAllOp1(ent : String ) : String pre: true post: result = type + "* getAll" + ent + "_" + name + "(struct " + ent + "* _col[])\n" + "{ int n = length((void**) _col);\n" + " " + type + "* result = (" + type + "*) calloc(n+1, sizeof(" + type + "));\n" + " int i = 0;\n" + " for ( ; i < n; i++)\n" + " { result[i] = get" + ent + "_" + name + "(_col[i]); }\n" + " result[n] = NULL;\n" + " return result;\n" + "}\n"; operation inheritedAllOp(ent : String , sup : String ) : String pre: true post: ( name /= "super" & type : CPrimitiveType => result = getAllOp(ent) ) & ( name /= "super" & type : CPointerType => result = getAllOp1(ent) ) & ( name = "super" => result = self.ancestorAllOps(ent,sup) ); operation ancestorAllOps(ent : String , sup : String ) : String pre: type : CPointerType post: anc = type.pointsTo & result = anc.members->collect( m | m.inheritedAllOp(ent,sup) )->sum(); operation inheritedAllOps(ent : String ) : String pre: type : CPointerType post: sup = type.pointsTo & result = sup.members->collect( m | m.inheritedAllOp(ent,sup.name) )->sum(); operation getPKOp(ent : String ) : String pre: true post: e = ent.toLowerCase & result = "struct " + ent + "* get" + ent + "ByPK(char* _ex)\n" + "{ int n = length((void**) " + e + "_instances);\n" + " int i = 0;\n" + " for ( ; i < n; i++)\n" + " { char* _v = get" + ent + "_" + name + "(" + e + "_instances[i]);\n" + " if (_v != NULL && strcmp(_v,_ex) == 0)\n" + " { return " + e + "_instances[i]; }\n" + " }\n" + " return NULL;\n" + "}\n"; operation getPKsOp(ent : String ) : String pre: true post: e = ent.toLowerCase & result = "struct " + ent + "** get" + ent + "ByPKs(char* _col[])\n" + "{ int n = length((void**) _col);\n" + " struct " + ent + "** result = (struct " + ent + "**) calloc(n+1, sizeof(struct " + ent + "*));\n" + " int i = 0; int j = 0;\n" + " for ( ; i < n; i++)\n" + " { char* _v = _col[i];\n" + " struct " + ent + "* _ex = get" + ent + "ByPK(_v);\n" + " if (_ex != NULL)\n" + " { result[j] = _ex; j++; }\n" + " }\n" + " result[j] = NULL;\n" + " return result; }\n"; operation initialiser() : String pre: true post: ( isKey = true => result = "" ) & ( name = "super" => result = " result->super = create" + type.pointsTo.name + "();\n" ) & ( type : CPointerType or type : CArrayType => result = " result->" + name + " = NULL;\n" ) & ( type : CPrimitiveType => result = " result->" + name + " = 0;\n" ); } class CVariable { attribute name : String; attribute kind : String; attribute initialisation : String; reference type : CType; } class CProgram { reference operations[*] : COperation; reference variables[*] : CVariable; reference structs[*] : CStruct; operation defineCOp(b : CExpression , par : String , pt : CType ) : COperation pre: true post: COperation->exists( op | op.name = "op_" + operations@pre.size & op.scope = "auxiliary" & op.isStatic = false & b.needsBracket = true & op.returnType = b.type & op.isQuery = true & CReturnStatement->exists( rt | rt.cstatId = "return_" + b.cexpId & b : rt.returnValue & op.code = rt ) & CVariable->exists( v | v.name = par & v.type = pt & v : op.parameters ) & op : operations & result = op ); operation printOperations() : void pre: true post: operations->forAll( op | op->display() ); operation printProgramHeader() : void pre: true post: "#include "->display() & "#include "->display() & "#include "->display() & "#include "->display() & "#include "->display() & "#include "->display() & "#include \"ocl.h\"\n"->display() & "#include \"app.h\"\n"->display(); } class COperation { attribute name : String; attribute opId : String; attribute isStatic : boolean; attribute scope : String; attribute isQuery : boolean; reference parameters[*] ordered : CVariable; reference returnType : CType; reference code : CStatement; operation parameterDeclaration(s : Sequence(CVariable) ) : String pre: true post: ( s.size = 0 => result = "void" ) & ( s.size = 1 => result = s[1].type + " " + s[1].name ) & ( s.size > 1 => result = s[1].type + " " + s[1].name + ", " + parameterDeclaration(s.tail) ); operation toString() : String pre: true post: result = returnType + " " + name + "(" + parameterDeclaration(parameters) + ")\n" + "{ " + code + "\n}\n"; operation getDeclaration() : String pre: true post: result = returnType + " " + name + "(" + parameterDeclaration(parameters) + ");\n"; } abstract class CStatement { attribute cstatId : String; operation toString() : String pre: true post: result = ""; } class CReturnStatement extends CStatement { reference returnValue[0-1] : CExpression; operation toString() : String pre: true post: ( returnValue.size >= 1 => result = "return " + returnValue.any + "; " ) & ( returnValue.size = 0 => result = "return; " ); } class CBreakStatement extends CStatement { operation toString() : String pre: true post: result = " break; "; } class OpCallStatement extends CStatement { attribute assignsTo : String; reference callExp : CExpression; operation toString() : String pre: true post: result = callExp + "; "; } abstract class CLoopStatement extends CStatement { reference test : CExpression; reference body : CStatement; } class ForLoop extends CLoopStatement { reference increment : CSequenceStatement; reference loopVar : CExpression; reference loopRange : CExpression; operation toString() : String pre: true post: ind = "ind_" + cstatId & result = "int " + ind + " = 0;\n" + "for ( ; " + ind + " < length((void**) " + loopRange + "); " + ind + "++)\n" + " { " + loopRange.elementType + " " + loopVar + " = (" + loopRange + ")[" + ind + "];\n" + " " + body + " } "; } class WhileLoop extends CLoopStatement { operation toString() : String pre: true post: result = "while (" + test + ")\n" + " { " + body + "}"; } class CAssignment extends CStatement { reference type[0-1] : CType; reference left : CExpression; reference right : CExpression; operation toString() : String pre: true post: ( type.size = 0 => result = left + " = " + right + "; " ) & ( type.size > 0 => result = type.any + " " + left + " = " + right + "; " ); } class CSequenceStatement extends CStatement { attribute kind : int; reference statements[*] ordered : CStatement; operation toString() : String pre: true post: ( statements.size > 1 => result = statements.front->collect( s | s.toString() + "\n " )->sum() + statements.last.toString() ) & ( statements.size = 1 => result = statements.last.toString() ) & ( true => result = "" ); } class IfStatement extends CStatement { reference test : CExpression; reference ifPart : CStatement; reference elsePart[0-1] : CStatement; operation toString() : String pre: true post: ( elsePart.size = 0 => result = "if (" + test + ")\n" + " { " + ifPart + " } " ) & ( elsePart.size > 0 => result = "if (" + test + ")\n" + " { " + ifPart + " }\n" + " else \n" + " { " + elsePart.any + " } " ); } class DeclarationStatement extends CStatement { attribute createsInstanceOf : String; attribute assignsTo : String; reference type : CType; reference elementType : CType; operation toString() : String pre: true post: ( createsInstanceOf = "String" => result = type + " " + assignsTo + " = \"\"; " ) & ( type : CPrimitiveType => result = type + " " + assignsTo + " = 0; " ) & ( true => result = type + " " + assignsTo + " = NULL; " ); } }