Merge branch 'master' into highprecision

vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POAssignmentDefinition.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.ProofObligationList;
 import com.fujitsu.vdmj.pog.SubTypeObligation;
 import com.fujitsu.vdmj.tc.lex.TCNameToken;
@@ -66,10 +67,11 @@ public TCType getType()
 	}
 
 	@Override
-	public ProofObligationList getProofObligations(POContextStack ctxt, Environment env)
+	public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
 	{
 		ProofObligationList obligations = new ProofObligationList();
 		obligations.addAll(expression.getProofObligations(ctxt, env));
+		obligations.stateUpdate(pogState, expression);
 
 		if (!TypeComparator.isSubType(ctxt.checkType(expression, expType), type))
 		{

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

@@ -32,6 +32,7 @@
 import com.fujitsu.vdmj.po.definitions.visitors.PODefinitionVisitor;
 import com.fujitsu.vdmj.po.definitions.visitors.POGetVariableNamesVisitor;
 import com.fujitsu.vdmj.pog.POContextStack;
+import com.fujitsu.vdmj.pog.POGState;
 import com.fujitsu.vdmj.pog.ProofObligationList;
 import com.fujitsu.vdmj.tc.lex.TCNameList;
 import com.fujitsu.vdmj.tc.lex.TCNameToken;
@@ -161,7 +162,9 @@ public boolean readsState()
 	abstract public TCType getType();
 
 	/**
-	 * Get a list of proof obligations for the definition.
+	 * 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).
 	 *
 	 * @param ctxt The call context.
 	 * @return A list of POs.
@@ -170,6 +173,11 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 	{
 		return new ProofObligationList();
 	}
+
+	public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
+	{
+		return getProofObligations(ctxt, env);	// Default to stateless version
+	}
 
 	/**
 	 * Implemented by all definitions to allow visitor processing.

vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/PODefinitionList.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.POLetDefContext;
 import com.fujitsu.vdmj.pog.PONameContext;
 import com.fujitsu.vdmj.pog.ProofObligationList;
@@ -72,6 +73,9 @@ 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();
@@ -86,6 +90,21 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 		return obligations;
 	}
 
+	/**
+	 * Get the proof obligations from every definition in the list and track POGState.
+	 */
+	public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
+	{
+		ProofObligationList obligations = new ProofObligationList();
+
+		for (PODefinition d: this)
+		{
+			obligations.addAll(d.getProofObligations(ctxt, pogState, env));
+		}
+
+		return obligations;
+	}
+
 	/**
 	 * This method gets obligations for each definition, but adds a context for each
 	 * one. This is used in let/def expressions, where definitions can depend on

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

@@ -24,9 +24,6 @@
 
 package com.fujitsu.vdmj.po.definitions;
 
-import java.util.List;
-import java.util.Vector;
-
 import com.fujitsu.vdmj.Release;
 import com.fujitsu.vdmj.Settings;
 import com.fujitsu.vdmj.lex.Dialect;
@@ -35,6 +32,7 @@
 import com.fujitsu.vdmj.po.expressions.POExpression;
 import com.fujitsu.vdmj.po.patterns.POPattern;
 import com.fujitsu.vdmj.po.patterns.POPatternList;
+import com.fujitsu.vdmj.po.patterns.POPatternListList;
 import com.fujitsu.vdmj.po.statements.POStatement;
 import com.fujitsu.vdmj.pog.OperationPostConditionObligation;
 import com.fujitsu.vdmj.pog.POContextStack;
@@ -213,9 +211,9 @@ else if (precondition != null)				// pre_op undefined in VDM++
 		return obligations;
 	}
 
-	public List<POPatternList> getParamPatternList()
+	public POPatternListList getParamPatternList()
 	{
-		List<POPatternList> list = new Vector<POPatternList>();
+		POPatternListList list = new POPatternListList();
 		list.add(parameterPatterns);
 		return list;
 	}

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

@@ -24,15 +24,13 @@
 
 package com.fujitsu.vdmj.po.definitions;
 
-import java.util.List;
-import java.util.Vector;
-
 import com.fujitsu.vdmj.po.annotations.POAnnotationList;
 import com.fujitsu.vdmj.po.definitions.visitors.PODefinitionVisitor;
 import com.fujitsu.vdmj.po.expressions.POExpression;
 import com.fujitsu.vdmj.po.expressions.PONotYetSpecifiedExpression;
 import com.fujitsu.vdmj.po.patterns.POPattern;
 import com.fujitsu.vdmj.po.patterns.POPatternList;
+import com.fujitsu.vdmj.po.patterns.POPatternListList;
 import com.fujitsu.vdmj.po.types.POPatternListTypePair;
 import com.fujitsu.vdmj.po.types.POPatternListTypePairList;
 import com.fujitsu.vdmj.po.types.POPatternTypePair;
@@ -214,9 +212,9 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 		return obligations;
 	}
 
-	public List<POPatternList> getParamPatternList()
+	public POPatternListList getParamPatternList()
 	{
-		List<POPatternList> list = new Vector<POPatternList>();
+		POPatternListList list = new POPatternListList();
 		POPatternList onelist = new POPatternList();
 
 		for (POPatternListTypePair p: parameterPatterns)

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

@@ -24,9 +24,6 @@
 
 package com.fujitsu.vdmj.po.definitions;
 
-import java.util.List;
-import java.util.Vector;
-
 import com.fujitsu.vdmj.Release;
 import com.fujitsu.vdmj.Settings;
 import com.fujitsu.vdmj.lex.Dialect;
@@ -35,6 +32,7 @@
 import com.fujitsu.vdmj.po.expressions.POExpression;
 import com.fujitsu.vdmj.po.patterns.POPattern;
 import com.fujitsu.vdmj.po.patterns.POPatternList;
+import com.fujitsu.vdmj.po.patterns.POPatternListList;
 import com.fujitsu.vdmj.po.statements.POErrorCaseList;
 import com.fujitsu.vdmj.po.statements.POExternalClauseList;
 import com.fujitsu.vdmj.po.statements.POStatement;
@@ -251,9 +249,9 @@ else if (precondition != null)				// pre_op state param undefined in VDM++
 		return obligations;
 	}
 
-	public List<POPatternList> getListParamPatternList()
+	public POPatternListList getListParamPatternList()
 	{
-		List<POPatternList> list = new Vector<POPatternList>();
+		POPatternListList list = new POPatternListList();
 
 		for (POPatternListTypePair p: parameterPatterns)
 		{

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

@@ -49,7 +49,7 @@ public POBlockStatement(LexLocation location, PODefinitionList assignmentDefs, P
 	@Override
 	public ProofObligationList getProofObligations(POContextStack ctxt, POGState pogState, Environment env)
 	{
-		ProofObligationList obligations = assignmentDefs.getProofObligations(ctxt, env);
+		ProofObligationList obligations = assignmentDefs.getProofObligations(ctxt, pogState, env);
 
 		ctxt.push(new POScopeContext());
 		obligations.addAll(super.getProofObligations(ctxt, pogState, env));

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

@@ -35,6 +35,7 @@ public class POGState
 	public POGState()
 	{
 		hasUpdatedState = false;
+		hasReadState = false;
 	}
 
 	private POGState(boolean hasUpdatedState, boolean hasReadState)
@@ -43,6 +44,13 @@ private POGState(boolean hasUpdatedState, boolean hasReadState)
 		this.hasReadState = hasReadState;
 	}
 
+	@Override
+	public String toString()
+	{
+		return (hasUpdatedState ? "has" : "has not") + " updated state; " +
+			   (hasReadState ?    "has" : "has not") + " read state";
+	}
+
 	public POGState getCopy()
 	{
 		return new POGState(hasUpdatedState, hasReadState);

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

@@ -24,11 +24,8 @@
 
 package com.fujitsu.vdmj.pog;
 
-import com.fujitsu.vdmj.po.definitions.POAssignmentDefinition;
 import com.fujitsu.vdmj.po.definitions.PODefinition;
 import com.fujitsu.vdmj.po.definitions.PODefinitionList;
-import com.fujitsu.vdmj.po.definitions.POValueDefinition;
-import com.fujitsu.vdmj.po.patterns.POIdentifierPattern;
 
 public class POLetDefContext extends POContext
 {
@@ -45,13 +42,6 @@ public POLetDefContext(PODefinition localDef)
 		this.localDefs.add(localDef);
 	}
 
-	public POLetDefContext(POAssignmentDefinition dcl)
-	{
-		this.localDefs = new PODefinitionList();
-		this.localDefs.add(new POValueDefinition(null,
-			new POIdentifierPattern(dcl.name), dcl.type, dcl.expression, dcl.expType, new PODefinitionList()));
-	}
-
 	@Override
 	public boolean isScopeBoundary()
 	{

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

@@ -41,6 +41,7 @@
 import com.fujitsu.vdmj.po.expressions.POExpression;
 import com.fujitsu.vdmj.po.patterns.POPattern;
 import com.fujitsu.vdmj.po.patterns.POPatternList;
+import com.fujitsu.vdmj.po.patterns.POPatternListList;
 import com.fujitsu.vdmj.tc.types.TCFunctionType;
 import com.fujitsu.vdmj.tc.types.TCType;
 import com.fujitsu.vdmj.tc.types.TCTypeList;
@@ -85,7 +86,7 @@ public ParameterPatternObligation(
 			generate(def.getListParamPatternList(), def.type.parameters, def.type.result));
 	}
 
-	private String generate(List<POPatternList> plist, TCTypeList params, TCType result)
+	private String generate(POPatternListList plist, TCTypeList params, TCType result)
 	{
 		StringBuilder foralls = new StringBuilder();
 		StringBuilder argnames = new StringBuilder();