Check operations for pure status in POGState

vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinition.java

@@ -62,6 +62,9 @@ public abstract class PODefinition extends PONode implements Serializable, Compa
 	/** A list of annotations, if any */
 	public POAnnotationList annotations = null;
 
+	/** A public/private/protected/static specifier, if any. */
+	public POAccessSpecifier accessSpecifier = null;
+
 	/**
 	 * Create a new definition of a particular name and location.
 	 */
@@ -75,6 +78,11 @@ public void setNameScope(NameScope scope)
 	{
 		this.nameScope = scope;
 	}
+
+	public void setAccessSpecifier(POAccessSpecifier specifier)
+	{
+		this.accessSpecifier = specifier;
+	}
 
 	@Override
 	abstract public String toString();

vdmj/src/main/java/com/fujitsu/vdmj/po/expressions/POApplyExpression.java

@@ -96,7 +96,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog
 		{
 			if (type.isOperation(location))
 			{
-				pogState.addExternals(location, opdef);
+				pogState.addOperation(location, opdef);
 			}
 
 			if (type.isMap(location))

vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallObjectStatement.java

@@ -78,7 +78,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog
 			obligations.addAll(exp.getProofObligations(ctxt, pogState, env));
 		}
 
-		pogState.addExternals(location, fdef);
+		pogState.addOperation(location, fdef);
 
 		return obligations;
 	}

vdmj/src/main/java/com/fujitsu/vdmj/po/statements/POCallStatement.java

@@ -66,7 +66,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog
 			obligations.addAll(exp.getProofObligations(ctxt, pogState, env));
 		}
 
-		pogState.addExternals(location, opdef);
+		pogState.addOperation(location, opdef);
 
 		return obligations;
 	}

vdmj/src/main/java/com/fujitsu/vdmj/po/statements/visitors/POStatementStateFinder.java

@@ -28,6 +28,7 @@
 import com.fujitsu.vdmj.lex.Token;
 import com.fujitsu.vdmj.po.POVisitorSet;
 import com.fujitsu.vdmj.po.definitions.PODefinition;
+import com.fujitsu.vdmj.po.definitions.POExplicitOperationDefinition;
 import com.fujitsu.vdmj.po.definitions.POImplicitOperationDefinition;
 import com.fujitsu.vdmj.po.definitions.POValueDefinition;
 import com.fujitsu.vdmj.po.definitions.visitors.PODefinitionStateFinder;
@@ -95,65 +96,13 @@ public TCNameSet caseAssignmentStatement(POAssignmentStatement node, Boolean upd
 	@Override
 	public TCNameSet caseCallStatement(POCallStatement node, Boolean updates)
 	{
-		TCNameSet all = newCollection();
-
-		if (node.opdef instanceof POImplicitOperationDefinition)
-		{
-			POImplicitOperationDefinition imp = (POImplicitOperationDefinition)node.opdef;
-
-			if (imp.externals != null)
-			{
-				for (POExternalClause ext: imp.externals)
-				{
-					if (updates && ext.mode.is(Token.WRITE))
-					{
-						all.addAll(ext.identifiers);
-					}
-					else if (!updates && ext.mode.is(Token.READ))
-					{
-						all.addAll(ext.identifiers);
-					}
-				}
-			}
-		}
-		else
-		{
-			all.add(EVERYTHING);	// Not state, but assumed to access state.
-		}
-
-		return all;
+		return operationCall(node.opdef, updates);
 	}
 
 	@Override
 	public TCNameSet caseCallObjectStatement(POCallObjectStatement node, Boolean updates)
 	{
-		TCNameSet all = newCollection();
-
-		if (node.fdef instanceof POImplicitOperationDefinition)
-		{
-			POImplicitOperationDefinition imp = (POImplicitOperationDefinition)node.fdef;
-
-			if (imp.externals != null)
-			{
-				for (POExternalClause ext: imp.externals)
-				{
-					if (updates && ext.mode.is(Token.WRITE))
-					{
-						all.addAll(ext.identifiers);
-					}
-					else if (!updates && ext.mode.is(Token.READ))
-					{
-						all.addAll(ext.identifiers);
-					}
-				}
-			}
-		}
-		else
-		{
-			all.add(EVERYTHING);	// Not state, but assumed to access state.
-		}
-
-		return all;
+		return operationCall(node.fdef, updates);
 	}
 
 	@Override
@@ -242,4 +191,51 @@ else if (sd instanceof POMapSeqDesignator)
 
 		return newCollection();		
 	}
+
+	/**
+	 * Use the operation's pure and ext clauses to try to determine the variable
+	 * access.
+	 */
+	private TCNameSet operationCall(PODefinition def, boolean updates)
+	{
+		TCNameSet all = newCollection();
+
+		if (def == null)
+		{
+			all.add(EVERYTHING);	// Don't know!
+		}
+		else if (def.accessSpecifier.isPure && updates)
+		{
+			// No updates by definition of pure
+		}
+		else if (def instanceof POImplicitOperationDefinition)
+		{
+			POImplicitOperationDefinition imp = (POImplicitOperationDefinition)def;
+
+			if (imp.externals != null)
+			{
+				for (POExternalClause ext: imp.externals)
+				{
+					if (updates && ext.mode.is(Token.WRITE))
+					{
+						all.addAll(ext.identifiers);
+					}
+					else if (!updates && ext.mode.is(Token.READ))
+					{
+						all.addAll(ext.identifiers);
+					}
+				}
+			}
+			else
+			{
+				all.add(EVERYTHING);
+			}
+		}
+		else if (def instanceof POExplicitOperationDefinition)
+		{
+			all.add(EVERYTHING);
+		}
+
+		return all;
+	}
 }

vdmj/src/main/java/com/fujitsu/vdmj/pog/POGState.java

@@ -26,6 +26,7 @@
 import com.fujitsu.vdmj.lex.LexLocation;
 import com.fujitsu.vdmj.lex.Token;
 import com.fujitsu.vdmj.po.definitions.PODefinition;
+import com.fujitsu.vdmj.po.definitions.POExplicitOperationDefinition;
 import com.fujitsu.vdmj.po.definitions.POImplicitOperationDefinition;
 import com.fujitsu.vdmj.po.statements.POExternalClause;
 import com.fujitsu.vdmj.tc.lex.TCNameList;
@@ -158,9 +159,13 @@ public void addDclLocal(TCNameToken name)
 		locals.add(name);
 	}
 
-	public void addExternals(LexLocation location, PODefinition called)
+	public void addOperation(LexLocation location, PODefinition called)
 	{
-		if (called instanceof POImplicitOperationDefinition)
+		if (called.accessSpecifier.isPure)
+		{
+			return;		// No updates, by definition
+		}
+		else if (called instanceof POImplicitOperationDefinition)
 		{
 			POImplicitOperationDefinition imp = (POImplicitOperationDefinition)called;
 
@@ -179,7 +184,7 @@ public void addExternals(LexLocation location, PODefinition called)
 				didUpdateState(location);
 			}
 		}
-		else
+		else if (called instanceof POExplicitOperationDefinition)
 		{
 			didUpdateState(location);
 		}

vdmj/src/main/resources/tc-po.mappings

@@ -16,29 +16,29 @@ map TCClassDefinition{annotations, name, classtype, definitions, invariant, hasC
 map TCClassInvariantDefinition{name, expression, classDefinition, nameScope} to POClassInvariantDefinition(name, expression, classDefinition) set nameScope;
 map TCClassList{} to POClassList(this);
 map TCCPUClassDefinition{classtype, definitions, invariant, hasConstructors, nameScope} to POCPUClassDefinition(classtype, definitions, invariant, hasConstructors, this) set nameScope;
-map TCDefinition{nameScope} to PODefinition() set nameScope;
-map TCEqualsDefinition{location, pattern, typebind, bind, test, expType, defType, defs, nameScope} to POEqualsDefinition(location, pattern, typebind, bind, test, expType, defType, defs) set nameScope;
-map TCExplicitFunctionDefinition{annotations, name, typeParams, type, paramPatternList, body, precondition, postcondition, isUndefined, expectedResult, actualResult, predef, postdef, paramDefinitionList, recursive, measureDef, measureName, nameScope} to POExplicitFunctionDefinition(annotations, name, typeParams, type, paramPatternList, body, precondition, postcondition, isUndefined, expectedResult, actualResult, predef, postdef, paramDefinitionList, recursive, measureDef, measureName) set nameScope;
-map TCExplicitOperationDefinition{annotations, name, type, parameterPatterns, paramDefinitions, actualResult, precondition, postcondition, body, isConstructor, predef, postdef, state, classDefinition, nameScope} to POExplicitOperationDefinition(annotations, name, type, parameterPatterns, precondition, postcondition, body, predef, postdef, paramDefinitions, state, classDefinition, actualResult, isConstructor) set nameScope;
-map TCExternalDefinition{state, readOnly, nameScope} to POExternalDefinition(state, readOnly) set nameScope;
-map TCImplicitFunctionDefinition{annotations, name, typeParams, parameterPatterns, type, result, body, precondition, postcondition, predef, postdef, recursive, isUndefined, actualResult, measureDef, measureName, nameScope} to POImplicitFunctionDefinition(annotations, name, typeParams, parameterPatterns, result, body, precondition, postcondition, type, predef, postdef, recursive, isUndefined, actualResult, measureDef, measureName) set nameScope;
-map TCImplicitOperationDefinition{annotations, name, parameterPatterns, result, body, externals, precondition, postcondition, errors, type, isConstructor, predef, postdef, state, actualResult, nameScope} to POImplicitOperationDefinition(annotations, name, parameterPatterns, result, body, externals, precondition, postcondition, errors, type, predef, postdef, actualResult, state, isConstructor) set nameScope;
-map TCImportedDefinition{location, def, nameScope} to POImportedDefinition(location, def) set nameScope;
-map TCInheritedDefinition{name, superdef, nameScope} to POInheritedDefinition(name, superdef) set nameScope;
-map TCInstanceVariableDefinition{name, type, expression, expType, nameScope} to POInstanceVariableDefinition(name, type, expression, expType) set nameScope;
-map TCLocalDefinition{location, name, type, nameScope} to POLocalDefinition(location, name, type) set nameScope;
-map TCMultiBindListDefinition{location, bindings, defs, nameScope} to POMultiBindListDefinition(location, bindings, defs) set nameScope;
-map TCMutexSyncDefinition{annotations, location, operations, nameScope} to POMutexSyncDefinition(annotations, location, operations) set nameScope;
-map TCNamedTraceDefinition{annotations, location, name, nameScope} to PONamedTraceDefinition(annotations, location, name) set nameScope;
-map TCPerSyncDefinition{annotations, location, opname, guard, nameScope} to POPerSyncDefinition(annotations, location, opname, guard) set nameScope;
-map TCRenamedDefinition{name, def, nameScope} to PORenamedDefinition(name, def) set nameScope;
-map TCStateDefinition{name, fields, invPattern, invExpression, initPattern, initExpression, invdef, initdef, recordType, nameScope} to POStateDefinition(name, fields, invPattern, invExpression, initPattern, initExpression, invdef, initdef, recordType) set nameScope;
-map TCSystemDefinition{name, classtype, definitions, nameScope} to POSystemDefinition(name, classtype, definitions, this) set nameScope;
-map TCThreadDefinition{statement, nameScope} to POThreadDefinition(statement) set nameScope;
-map TCTypeDefinition{annotations, name, type, invPattern, invExpression, invdef, eqPattern1, eqPattern2, eqExpression, eqdef, ordPattern1, ordPattern2, ordExpression, orddef, nameScope} to POTypeDefinition(annotations, name, type, invPattern, invExpression, invdef, eqPattern1, eqPattern2, eqExpression, eqdef, ordPattern1, ordPattern2, ordExpression, orddef) set nameScope;
-map TCValueDefinition{annotations, pattern, type, exp, expType, defs, nameScope} to POValueDefinition(annotations, pattern, type, exp, expType, defs) set nameScope;
-map TCUntypedDefinition{location, name, nameScope} to POUntypedDefinition(location, name) set nameScope;
-map TCQualifiedDefinition{def, type, nameScope} to POQualifiedDefinition(def, type) set nameScope;
+map TCDefinition{} to PODefinition();
+map TCEqualsDefinition{accessSpecifier, location, pattern, typebind, bind, test, expType, defType, defs, nameScope} to POEqualsDefinition(location, pattern, typebind, bind, test, expType, defType, defs) set nameScope, accessSpecifier;
+map TCExplicitFunctionDefinition{accessSpecifier, annotations, name, typeParams, type, paramPatternList, body, precondition, postcondition, isUndefined, expectedResult, actualResult, predef, postdef, paramDefinitionList, recursive, measureDef, measureName, nameScope} to POExplicitFunctionDefinition(annotations, name, typeParams, type, paramPatternList, body, precondition, postcondition, isUndefined, expectedResult, actualResult, predef, postdef, paramDefinitionList, recursive, measureDef, measureName) set nameScope, accessSpecifier;
+map TCExplicitOperationDefinition{accessSpecifier, annotations, name, type, parameterPatterns, paramDefinitions, actualResult, precondition, postcondition, body, isConstructor, predef, postdef, state, classDefinition, nameScope} to POExplicitOperationDefinition(annotations, name, type, parameterPatterns, precondition, postcondition, body, predef, postdef, paramDefinitions, state, classDefinition, actualResult, isConstructor) set nameScope, accessSpecifier;
+map TCExternalDefinition{accessSpecifier, state, readOnly, nameScope} to POExternalDefinition(state, readOnly) set nameScope, accessSpecifier;
+map TCImplicitFunctionDefinition{accessSpecifier, annotations, name, typeParams, parameterPatterns, type, result, body, precondition, postcondition, predef, postdef, recursive, isUndefined, actualResult, measureDef, measureName, nameScope} to POImplicitFunctionDefinition(annotations, name, typeParams, parameterPatterns, result, body, precondition, postcondition, type, predef, postdef, recursive, isUndefined, actualResult, measureDef, measureName) set nameScope, accessSpecifier;
+map TCImplicitOperationDefinition{accessSpecifier, annotations, name, parameterPatterns, result, body, externals, precondition, postcondition, errors, type, isConstructor, predef, postdef, state, actualResult, nameScope} to POImplicitOperationDefinition(annotations, name, parameterPatterns, result, body, externals, precondition, postcondition, errors, type, predef, postdef, actualResult, state, isConstructor) set nameScope, accessSpecifier;
+map TCImportedDefinition{accessSpecifier, location, def, nameScope} to POImportedDefinition(location, def) set nameScope, accessSpecifier;
+map TCInheritedDefinition{accessSpecifier, name, superdef, nameScope} to POInheritedDefinition(name, superdef) set nameScope, accessSpecifier;
+map TCInstanceVariableDefinition{accessSpecifier, name, type, expression, expType, nameScope} to POInstanceVariableDefinition(name, type, expression, expType) set nameScope, accessSpecifier;
+map TCLocalDefinition{accessSpecifier, location, name, type, nameScope} to POLocalDefinition(location, name, type) set nameScope, accessSpecifier;
+map TCMultiBindListDefinition{accessSpecifier, location, bindings, defs, nameScope} to POMultiBindListDefinition(location, bindings, defs) set nameScope, accessSpecifier;
+map TCMutexSyncDefinition{accessSpecifier, annotations, location, operations, nameScope} to POMutexSyncDefinition(annotations, location, operations) set nameScope, accessSpecifier;
+map TCNamedTraceDefinition{accessSpecifier, annotations, location, name, nameScope} to PONamedTraceDefinition(annotations, location, name) set nameScope, accessSpecifier;
+map TCPerSyncDefinition{accessSpecifier, annotations, location, opname, guard, nameScope} to POPerSyncDefinition(annotations, location, opname, guard) set nameScope, accessSpecifier;
+map TCRenamedDefinition{accessSpecifier, name, def, nameScope} to PORenamedDefinition(name, def) set nameScope, accessSpecifier;
+map TCStateDefinition{accessSpecifier, name, fields, invPattern, invExpression, initPattern, initExpression, invdef, initdef, recordType, nameScope} to POStateDefinition(name, fields, invPattern, invExpression, initPattern, initExpression, invdef, initdef, recordType) set nameScope, accessSpecifier;
+map TCSystemDefinition{accessSpecifier, name, classtype, definitions, nameScope} to POSystemDefinition(name, classtype, definitions, this) set nameScope, accessSpecifier;
+map TCThreadDefinition{accessSpecifier, statement, nameScope} to POThreadDefinition(statement) set nameScope, accessSpecifier;
+map TCTypeDefinition{accessSpecifier, annotations, name, type, invPattern, invExpression, invdef, eqPattern1, eqPattern2, eqExpression, eqdef, ordPattern1, ordPattern2, ordExpression, orddef, nameScope} to POTypeDefinition(annotations, name, type, invPattern, invExpression, invdef, eqPattern1, eqPattern2, eqExpression, eqdef, ordPattern1, ordPattern2, ordExpression, orddef) set nameScope, accessSpecifier;
+map TCValueDefinition{accessSpecifier, annotations, pattern, type, exp, expType, defs, nameScope} to POValueDefinition(annotations, pattern, type, exp, expType, defs) set nameScope, accessSpecifier;
+map TCUntypedDefinition{accessSpecifier, location, name, nameScope} to POUntypedDefinition(location, name) set nameScope, accessSpecifier;
+map TCQualifiedDefinition{accessSpecifier, def, type, nameScope} to POQualifiedDefinition(def, type) set nameScope, accessSpecifier;
 
 # expressions
 package com.fujitsu.vdmj.tc.expressions to com.fujitsu.vdmj.po.expressions;