Merge branch 'master' into highprecision

vdmj/documentation/MESSAGES

@@ -400,12 +400,14 @@ as the expected and actual values.
 2327, "Type set1 is not available in classic"
 2328, "Sequence binds are not available in classic"
 2329, "Duplicate <keyword> keyword"
-2330, "Tokens found after expression at <token>"
+2330, "POG: Tokens found after obligation at <token>"
 2331, "Expecting inv, eq or ord clause"
 2332, "Duplicate inv clause"
 2333, "Type eq/ord clauses not available in classic"
 2334, "Failed to instantiate AST<name>Annotation"
 2335, "Maximal '!' not allowed here"
+2336, "POG: Obligation is not boolean?"
+2337, "POG Obligation has type errors?"
 
 
 3000, "Expression does not match declared type"

vdmj/src/main/java/com/fujitsu/vdmj/po/annotations/POAnnotatedExpression.java

@@ -28,6 +28,7 @@
 import com.fujitsu.vdmj.po.expressions.POExpression;
 import com.fujitsu.vdmj.po.expressions.visitors.POExpressionVisitor;
 import com.fujitsu.vdmj.pog.POContextStack;
+import com.fujitsu.vdmj.pog.POGState;
 import com.fujitsu.vdmj.pog.ProofObligationList;
 import com.fujitsu.vdmj.typechecker.Environment;
 
@@ -53,10 +54,10 @@ public String toString()
 	}
 
 	@Override
-	public ProofObligationList getProofObligations(POContextStack ctxt, Environment env)
+	public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
 	{
 		annotation.poBefore(this, ctxt);
-		ProofObligationList obligations = expression.getProofObligations(ctxt, env);
+		ProofObligationList obligations = expression.getProofObligations(ctxt, pogState, env);
 		annotation.poAfter(this, obligations, ctxt);
 		return obligations;
 	}

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

@@ -70,7 +70,7 @@ public TCType getType()
 	public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
 	{
 		ProofObligationList obligations = new ProofObligationList();
-		obligations.addAll(expression.getProofObligations(ctxt, env));
+		obligations.addAll(expression.getProofObligations(ctxt, pogState, env));
 		obligations.stateUpdate(pogState, expression);
 
 		if (!TypeComparator.isSubType(ctxt.checkType(expression, expType), type))

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

@@ -28,6 +28,7 @@
 import com.fujitsu.vdmj.po.definitions.visitors.PODefinitionVisitor;
 import com.fujitsu.vdmj.po.statements.POClassInvariantStatement;
 import com.fujitsu.vdmj.pog.POContextStack;
+import com.fujitsu.vdmj.pog.POGState;
 import com.fujitsu.vdmj.pog.ProofObligationList;
 import com.fujitsu.vdmj.tc.definitions.TCClassDefinition;
 import com.fujitsu.vdmj.tc.lex.TCNameToken;
@@ -172,14 +173,19 @@ public boolean hasNew()
 	}
 
 	@Override
-	public ProofObligationList getProofObligations(POContextStack ctxt, Environment publicEnv)
+	public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment publicEnv)
 	{
 		ProofObligationList list =
 				(annotations != null) ? annotations.poBefore(this) : new ProofObligationList();
 
 		Environment env = new PrivateClassEnvironment(tcdef, publicEnv);
 		Environment local = new FlatEnvironment(tcdef.getSelfDefinition(), env);
-		list.addAll(definitions.getProofObligations(ctxt, local));
+
+		for (PODefinition def: definitions)
+		{
+			list.addAll(def.getProofObligations(new POContextStack(), new POGState(), local));
+		}
+
 		list.typeCheck(tcdef.name, local);
 
 		if (annotations != null) annotations.poAfter(this, list);

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

@@ -27,6 +27,7 @@
 import com.fujitsu.vdmj.po.definitions.visitors.PODefinitionVisitor;
 import com.fujitsu.vdmj.po.expressions.POExpression;
 import com.fujitsu.vdmj.pog.POContextStack;
+import com.fujitsu.vdmj.pog.POGState;
 import com.fujitsu.vdmj.pog.ProofObligation;
 import com.fujitsu.vdmj.pog.ProofObligationList;
 import com.fujitsu.vdmj.pog.StateInvariantObligation;
@@ -63,7 +64,7 @@ public String toString()
 	}
 
 	@Override
-	public ProofObligationList getProofObligations(POContextStack ctxt, Environment env)
+	public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
 	{
 		ProofObligationList list = new ProofObligationList();
 

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

@@ -26,6 +26,7 @@
 
 import com.fujitsu.vdmj.po.POMappedList;
 import com.fujitsu.vdmj.pog.POContextStack;
+import com.fujitsu.vdmj.pog.POGState;
 import com.fujitsu.vdmj.pog.ProofObligationList;
 import com.fujitsu.vdmj.tc.definitions.TCClassDefinition;
 import com.fujitsu.vdmj.tc.definitions.TCClassList;
@@ -72,7 +73,7 @@ public ProofObligationList getProofObligations()
 
 		for (POClassDefinition c: this)
 		{
-			obligations.addAll(c.getProofObligations(new POContextStack(), new PublicClassEnvironment(tcclasses)));
+			obligations.addAll(c.getProofObligations(new POContextStack(), new POGState(), new PublicClassEnvironment(tcclasses)));
 		}
 
 		return obligations;

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

@@ -130,22 +130,6 @@ public final TCNameList getVariableNames()
 		list.addAll(apply(new POGetVariableNamesVisitor(), null));
 		return list;
 	}
-
-	/**
-	 * True, if the definition contains executable statements that update state.
-	 */
-	public boolean updatesState()
-	{
-		return false;
-	}
-
-	/**
-	 * True, if the definition contains executable statements that read state.
-	 */
-	public boolean readsState()
-	{
-		return false;
-	}
 
 	/**
 	 * Return the static type of the definition. For example, the type of a
@@ -162,21 +146,15 @@ public boolean readsState()
 	abstract public TCType getType();
 
 	/**
-	 * Get a list of proof obligations for the definition. The second method is used
-	 * to track the POG state for updates to state variables, which is only used
-	 * by a few definition types (eg. POAssignmentDefinitions).
+	 * Get a list of proof obligations for the definition.
 	 *
 	 * @param ctxt The call context.
+	 * @param pogState Tracks updates to state in operations.
 	 * @return A list of POs.
 	 */
-	public ProofObligationList getProofObligations(POContextStack ctxt, Environment env)
-	{
-		return new ProofObligationList();
-	}
-
 	public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
 	{
-		return getProofObligations(ctxt, env);	// Default to stateless version
+		return new ProofObligationList();
 	}
 
 	/**

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

@@ -28,7 +28,6 @@
 import com.fujitsu.vdmj.pog.POContextStack;
 import com.fujitsu.vdmj.pog.POGState;
 import com.fujitsu.vdmj.pog.POLetDefContext;
-import com.fujitsu.vdmj.pog.PONameContext;
 import com.fujitsu.vdmj.pog.ProofObligationList;
 import com.fujitsu.vdmj.tc.definitions.TCDefinition;
 import com.fujitsu.vdmj.tc.definitions.TCDefinitionList;
@@ -73,23 +72,6 @@ public String toString()
 		return sb.toString();
 	}
 
-	/**
-	 * Get the proof obligations from every definition in the list.
-	 */
-	public ProofObligationList getProofObligations(POContextStack ctxt, Environment env)
-	{
-		ProofObligationList obligations = new ProofObligationList();
-
-		for (PODefinition d: this)
-		{
-			ctxt.push(new PONameContext(d.getVariableNames()));
-			obligations.addAll(d.getProofObligations(ctxt, env));
-			ctxt.pop();
-		}
-
-		return obligations;
-	}
-
 	/**
 	 * Get the proof obligations from every definition in the list and track POGState.
 	 */
@@ -110,7 +92,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, POGState pog
 	 * one. This is used in let/def expressions, where definitions can depend on
 	 * earlier definitions in the same expression.
 	 */
-	public ProofObligationList getDefProofObligations(POContextStack ctxt, Environment env)
+	public ProofObligationList getDefProofObligations(POContextStack ctxt, POGState pogState, Environment env)
 	{
 		ProofObligationList obligations = new ProofObligationList();
 		int count = 0;
@@ -120,9 +102,7 @@ public ProofObligationList getDefProofObligations(POContextStack ctxt, Environme
 			ctxt.push(new POLetDefContext(d));		// In scope for recursive or total obligations
 			count++;
 
-			ctxt.push(new PONameContext(d.getVariableNames()));
-			obligations.addAll(d.getProofObligations(ctxt, env));
-			ctxt.pop();
+			obligations.addAll(d.getProofObligations(ctxt, pogState, env));
 		}
 
 		for (int i=0; i<count; i++)

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

@@ -35,6 +35,7 @@
 import com.fujitsu.vdmj.po.patterns.POSetBind;
 import com.fujitsu.vdmj.po.patterns.POTypeBind;
 import com.fujitsu.vdmj.pog.POContextStack;
+import com.fujitsu.vdmj.pog.POGState;
 import com.fujitsu.vdmj.pog.ProofObligationList;
 import com.fujitsu.vdmj.pog.SeqMemberObligation;
 import com.fujitsu.vdmj.pog.SetMemberObligation;
@@ -107,7 +108,7 @@ public int hashCode()
 	}
 
 	@Override
-	public ProofObligationList getProofObligations(POContextStack ctxt, Environment env)
+	public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
 	{
 		ProofObligationList list = new ProofObligationList();
 
@@ -151,16 +152,16 @@ else if (typebind != null)
 		}
 		else if (bind instanceof POSetBind)
 		{
-			list.addAll(((POSetBind)bind).set.getProofObligations(ctxt, env));
+			list.addAll(((POSetBind)bind).set.getProofObligations(ctxt, pogState, env));
 			list.add(new SetMemberObligation(test, ((POSetBind)bind).set, ctxt));
 		}
 		else if (bind instanceof POSeqBind)
 		{
-			list.addAll(((POSeqBind)bind).sequence.getProofObligations(ctxt, env));
+			list.addAll(((POSeqBind)bind).sequence.getProofObligations(ctxt, pogState, env));
 			list.add(new SeqMemberObligation(test, ((POSeqBind)bind).sequence, ctxt));
 		}
 
-		list.addAll(test.getProofObligations(ctxt, env));
+		list.addAll(test.getProofObligations(ctxt, pogState, env));
 		return list;
 	}
 

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

@@ -37,6 +37,7 @@
 import com.fujitsu.vdmj.pog.POContextStack;
 import com.fujitsu.vdmj.pog.POFunctionDefinitionContext;
 import com.fujitsu.vdmj.pog.POFunctionResultContext;
+import com.fujitsu.vdmj.pog.POGState;
 import com.fujitsu.vdmj.pog.PONameContext;
 import com.fujitsu.vdmj.pog.ParameterPatternObligation;
 import com.fujitsu.vdmj.pog.ProofObligationList;
@@ -134,7 +135,7 @@ public TCType getType()
 	}
 
 	@Override
-	public ProofObligationList getProofObligations(POContextStack ctxt, Environment env)
+	public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
 	{
 		ProofObligationList obligations =
 				(annotations != null) ? annotations.poBefore(this, ctxt) : new ProofObligationList();
@@ -170,7 +171,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 		if (precondition != null)
 		{
 			ctxt.push(new POFunctionDefinitionContext(this, false));
-			obligations.addAll(precondition.getProofObligations(ctxt, env));
+			obligations.addAll(precondition.getProofObligations(ctxt, pogState, env));
 			ctxt.pop();
 		}
 
@@ -181,7 +182,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 				ctxt.push(new POFunctionDefinitionContext(this, false));
 				obligations.add(new FuncPostConditionObligation(this, ctxt));
 				ctxt.push(new POFunctionResultContext(this));
-				obligations.addAll(postcondition.getProofObligations(ctxt, env));
+				obligations.addAll(postcondition.getProofObligations(ctxt, pogState, env));
 				ctxt.pop();
 				ctxt.pop();
 			}
@@ -190,12 +191,12 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 		if (measureDef != null && measureName != null && measureName.isMeasureName())
 		{
 			ctxt.push(new PONameContext(new TCNameList(measureName)));
-			obligations.addAll(measureDef.getProofObligations(ctxt, env));
+			obligations.addAll(measureDef.getProofObligations(ctxt, pogState, env));
 			ctxt.pop();
 		}
 
 		ctxt.push(new POFunctionDefinitionContext(this, true));
-		ProofObligationList bodyObligations = body.getProofObligations(ctxt, env);
+		ProofObligationList bodyObligations = body.getProofObligations(ctxt, pogState, env);
 		bodyObligationCount  = bodyObligations.size();
 		obligations.addAll(bodyObligations);
 

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

@@ -117,7 +117,7 @@ public TCType getType()
 	}
 
 	@Override
-	public ProofObligationList getProofObligations(POContextStack ctxt, Environment env)
+	public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
 	{
 		ProofObligationList obligations =
 				(annotations != null) ? annotations.poBefore(this, ctxt) : new ProofObligationList();
@@ -140,7 +140,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 		 */
 		if (precondition != null && Settings.dialect == Dialect.VDM_SL)
 		{
-			obligations.addAll(predef.getProofObligations(ctxt, env));
+			obligations.addAll(predef.getProofObligations(ctxt, pogState, env));
 		}
 
 		if (postcondition != null && Settings.dialect == Dialect.VDM_SL)
@@ -155,24 +155,22 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 			}
 			else
 			{
-				obligations.addAll(postdef.getProofObligations(ctxt, env));
+				obligations.addAll(postdef.getProofObligations(ctxt, pogState, env));
 			}
 
 			obligations.add(new OperationPostConditionObligation(this, ctxt));
 		}
 
-		POGState pstate = new POGState();
-
 		if (stateDefinition != null)
 		{
 			ctxt.push(new POOperationDefinitionContext(this, (precondition != null), stateDefinition, true));
-			obligations.addAll(body.getProofObligations(ctxt, pstate, env));
+			obligations.addAll(body.getProofObligations(ctxt, pogState, env));
 			ctxt.pop();
 		}
 		else if (classDefinition != null)
 		{
 			ctxt.push(new POOperationDefinitionContext(this, (precondition != null), classDefinition, true));
-			ProofObligationList oblist = body.getProofObligations(ctxt, pstate, env);
+			ProofObligationList oblist = body.getProofObligations(ctxt, pogState, env);
 			ctxt.pop();
 
 			if (Settings.release != Release.VDM_10)		// Uses the obj_C pattern in OperationDefContext
@@ -189,7 +187,7 @@ else if (precondition != null)				// pre_op undefined in VDM++
 		else	// Flat spec with no state defined
 		{
 			ctxt.push(new POOperationDefinitionContext(this, (precondition != null), null, true));
-			obligations.addAll(body.getProofObligations(ctxt, pstate, env));
+			obligations.addAll(body.getProofObligations(ctxt, pogState, env));
 			ctxt.pop();
 		}
 
@@ -217,18 +215,6 @@ public POPatternListList getParamPatternList()
 		list.add(parameterPatterns);
 		return list;
 	}
-
-	@Override
-	public boolean updatesState()
-	{
-		return body.updatesState();
-	}
-
-	@Override
-	public boolean readsState()
-	{
-		return body.readsState();
-	}
 
 	@Override
 	public <R, S> R apply(PODefinitionVisitor<R, S> visitor, S arg)