Merge branch 'master' into highprecision

# Conflicts:
#	vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INSetRangeExpression.java

quickcheck/src/main/java/quickcheck/QuickCheck.java

@@ -408,7 +408,8 @@ public void checkObligation(ProofObligation po, StrategyResults sresults)
 
 			if (!po.isCheckable)
 			{
-				infof(POStatus.UNCHECKED, "PO #%d, UNCHECKED\n", po.number);
+				infof(POStatus.UNCHECKED, "PO #%d, UNCHECKED %s\n",
+					po.number, (po.message == null ? "" : "(" + po.message + ")"));
 				return;
 			}
 			else if (sresults.provedBy != null)

quickcheck/src/main/java/quickcheck/visitors/FixedRangeCreator.java

@@ -193,7 +193,7 @@ public ValueSet caseNaturalOneType(TCNaturalOneType node, Integer limit)
 		{
 			try
 			{
-				result.addNoSort(new NaturalOneValue(a));
+				result.addSorted(new NaturalOneValue(a));
 			}
 			catch (Exception e)
 			{
@@ -213,7 +213,7 @@ public ValueSet caseNaturalType(TCNaturalType node, Integer limit)
 		{
 			try
 			{
-				result.addNoSort(new NaturalValue(a));
+				result.addSorted(new NaturalValue(a));
 			}
 			catch (Exception e)
 			{
@@ -235,11 +235,11 @@ public ValueSet caseIntegerType(TCIntegerType node, Integer limit)
 			case 1:		return new ValueSet(new IntegerValue(0));
 			default:
 				int a = -limit/2;
-				result.addNoSort(new IntegerValue(a++));
+				result.addSorted(new IntegerValue(a++));
 
 				while (result.size() < limit)
 				{
-					result.addNoSort(new IntegerValue(a));
+					result.addSorted(new IntegerValue(a));
 					a++;
 				}
 

quickcheck/src/main/java/quickcheck/visitors/RangeCreator.java

@@ -115,26 +115,37 @@ protected List<ValueSet> powerLimit(ValueSet source, int limit, boolean incEmpty
 
 	/**
 	 * Return the lowest integer power of n that is &lt;= limit. If n &lt; 2,
-	 * just return 1.
+	 * just return limit.
+	 * 
+	 * Used to calculate how many field values to generate for an n-field object.
+	 * For example, a three field tuple/record with one value each gives 1x1x1=1 records;
+	 * with two values each it gives 2x2x2=8 values, with three 3x3x3=27 values. So to
+	 * generate up to N values from F field combinations, we need to find the largest n,
+	 * such that n^F < N.
+	 * 
+	 * If there is only one field, we can generate N values.
 	 */
-	protected int leastPower(int n, int limit)
+	protected int leastPower(int F, int N)
 	{
-		int power = 1;
-
-		if (n > 1)
+		if (F > 1)
 		{
-			int value = n;
+			int power = 1;
+			int value = F;
 
-			while (value < limit)
+			while (value < N)
 			{
-				value = value * n;
+				value = value * F;
 				power++;
 			}
+
+			return power - 1;
+		}
+		else
+		{
+			return N;
 		}
-
-		return power;
 	}
-	
+
 	/**
 	 * Attempt to produce a function that matches a (possibly polymorphic) TCFunctionType.
 	 */

vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INIndicesExpression.java

@@ -61,10 +61,10 @@ public Value eval(Context ctxt)
 
     		for (int i=1; i<= seq.size(); i++)
     		{
-    			result.addNoCheck(new NaturalOneValue(i));
+    			result.addSorted(new NaturalOneValue(i));
     		}
 
-    		return new SetValue(result);
+    		return new SetValue(result, false);
         }
         catch (ValueException e)
         {

vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INPowerSetExpression.java

@@ -65,7 +65,7 @@ public Value eval(Context ctxt)
 
     		for (ValueSet v: psets)
     		{
-    			rs.addNoCheck(new SetValue(v));
+    			rs.addSorted(new SetValue(v, false));	// Already sorted
     		}
 
     		// The additions above can take a while, because all of the SetValues are

vdmj/src/main/java/com/fujitsu/vdmj/in/expressions/INSetRangeExpression.java

@@ -67,7 +67,7 @@ public Value eval(Context ctxt)
 
     		while (from.compareTo(to) <= 0)
     		{
-    			set.addNoCheck(new IntegerValue(from));
+    			set.addSorted(new IntegerValue(from));
     			from = from.add(BigInteger.ONE);
     		}
 

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

@@ -73,8 +73,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 
 		if (!TypeComparator.isSubType(ctxt.checkType(expression, expType), type))
 		{
-			obligations.add(
-				new SubTypeObligation(expression, type, expType, ctxt));
+			obligations.add(new SubTypeObligation(expression, type, expType, ctxt));
 		}
 
 		return obligations;

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

@@ -27,7 +27,6 @@
 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.PONoCheckContext;
 import com.fujitsu.vdmj.pog.ProofObligationList;
 import com.fujitsu.vdmj.pog.StateInvariantObligation;
 import com.fujitsu.vdmj.tc.lex.TCNameToken;
@@ -69,9 +68,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 
 		if (!classDefinition.hasConstructors)
 		{
-			ctxt.push(new PONoCheckContext());
 			list.add(new StateInvariantObligation(this, ctxt));
-			ctxt.pop();
 		}
 
 		return list;

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

@@ -35,14 +35,15 @@
 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.statements.POSimpleBlockStatement;
 import com.fujitsu.vdmj.po.statements.POStatement;
 import com.fujitsu.vdmj.pog.OperationPostConditionObligation;
 import com.fujitsu.vdmj.pog.POContextStack;
 import com.fujitsu.vdmj.pog.POFunctionDefinitionContext;
 import com.fujitsu.vdmj.pog.POImpliesContext;
-import com.fujitsu.vdmj.pog.PONoCheckContext;
 import com.fujitsu.vdmj.pog.POOperationDefinitionContext;
 import com.fujitsu.vdmj.pog.ParameterPatternObligation;
+import com.fujitsu.vdmj.pog.ProofObligation;
 import com.fujitsu.vdmj.pog.ProofObligationList;
 import com.fujitsu.vdmj.pog.StateInvariantObligation;
 import com.fujitsu.vdmj.pog.SubTypeObligation;
@@ -159,83 +160,71 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 				obligations.addAll(postdef.getProofObligations(ctxt, env));
 			}
 
-			ctxt.push(new PONoCheckContext());
 			obligations.add(new OperationPostConditionObligation(this, ctxt));
-			ctxt.pop();
 		}
 
-		boolean updatesState = body.updatesState();
+		boolean updatesState = !(body instanceof POSimpleBlockStatement) && body.updatesState();
 
 		if (stateDefinition != null)
 		{
-			if (!updatesState)
+			ctxt.push(new POOperationDefinitionContext(this, (precondition != null), stateDefinition, true));
+			ProofObligationList oblist = body.getProofObligations(ctxt, null, env);
+			ctxt.pop();
+
+			if (updatesState)
 			{
-				ctxt.push(new POOperationDefinitionContext(this, (precondition != null), stateDefinition, true));
-				obligations.addAll(body.getProofObligations(ctxt, null, env));
-				ctxt.pop();
-			}
-			else
-			{
-				ctxt.push(new PONoCheckContext());
-				ctxt.push(new POOperationDefinitionContext(this, (precondition != null), stateDefinition, true));
-				obligations.addAll(body.getProofObligations(ctxt, null, env));
-				ctxt.pop();
-				ctxt.pop();
+				oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE);
 			}
+
+			obligations.addAll(oblist);
 		}
 		else if (classDefinition != null)
 		{
-			if (Settings.release == Release.VDM_10)		// Uses the obj_C pattern
+			ctxt.push(new POOperationDefinitionContext(this, (precondition != null), classDefinition, true));
+			ProofObligationList oblist = body.getProofObligations(ctxt, null, env);
+			ctxt.pop();
+
+			if (Settings.release != Release.VDM_10)		// Uses the obj_C pattern in OperationDefContext
+			{
+				oblist.markUnchecked(ProofObligation.REQUIRES_VDM10);
+			}
+			else if (precondition != null)				// pre_op undefined in VDM++
 			{
-				if (precondition == null && !updatesState)
-				{
-					ctxt.push(new POOperationDefinitionContext(this, false, classDefinition, true));
-					obligations.addAll(body.getProofObligations(ctxt, null, env));
-					ctxt.pop();
-				}
-				else	// Can't check "pre_op(args, new X(args)) => ..."
-				{
-					ctxt.push(new PONoCheckContext());
-					ctxt.push(new POOperationDefinitionContext(this, true, classDefinition, true));
-					obligations.addAll(body.getProofObligations(ctxt, null, env));
-					ctxt.pop();
-					ctxt.pop();
-				}
+				oblist.markUnchecked(ProofObligation.UNCHECKED_VDMPP);
 			}
+			else if (updatesState)
+			{
+				oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE);
+			}
+
+			obligations.addAll(oblist);
 		}
 		else	// Flat spec with no state defined
 		{
-			if (!updatesState)
-			{
-				ctxt.push(new POOperationDefinitionContext(this, (precondition != null), null, true));
-				obligations.addAll(body.getProofObligations(ctxt, null, env));
-				ctxt.pop();
-			}
-			else
+			ctxt.push(new POOperationDefinitionContext(this, (precondition != null), null, true));
+			ProofObligationList oblist = body.getProofObligations(ctxt, null, env);
+			ctxt.pop();
+
+			if (updatesState)
 			{
-				ctxt.push(new PONoCheckContext());
-				ctxt.push(new POOperationDefinitionContext(this, (precondition != null), null, true));
-				obligations.addAll(body.getProofObligations(ctxt, null, env));
-				ctxt.pop();
-				ctxt.pop();
+				oblist.markUnchecked(ProofObligation.BODY_UPDATES_STATE);
 			}
+
+			obligations.addAll(oblist);
 		}
 
 		if (isConstructor &&
 			classDefinition != null &&
 			classDefinition.invariant != null)
 		{
-			ctxt.push(new PONoCheckContext());
 			obligations.add(new StateInvariantObligation(this, ctxt));
-			ctxt.pop();
 		}
 
 		if (!isConstructor &&
 			!TypeComparator.isSubType(actualResult, type.result))
 		{
-			ctxt.push(new PONoCheckContext());
-			obligations.add(new SubTypeObligation(this, actualResult, ctxt));
-			ctxt.pop();
+			obligations.add(new SubTypeObligation(this, actualResult, ctxt).
+				markUnchecked(ProofObligation.NOT_YET_SUPPORTED));
 		}
 
 		if (annotations != null) annotations.poAfter(this, obligations, ctxt);