Merge branch 'master' into highprecision

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

@@ -70,7 +70,7 @@
 import annotations.IterableContext;
 import annotations.po.POQuickCheckAnnotation;
 import quickcheck.strategies.QCStrategy;
-import quickcheck.strategies.Results;
+import quickcheck.strategies.StrategyResults;
 import quickcheck.visitors.FixedRangeCreator;
 import quickcheck.visitors.TypeBindFinder;
 
@@ -308,29 +308,35 @@ public List<INBindingSetter> getINBindList(INExpression inexp)
 		return inexp.apply(new TypeBindFinder(), null);
 	}
 
-	public Results getValues(ProofObligation po)
+	public StrategyResults getValues(ProofObligation po)
 	{
 		Map<String, ValueList> union = new HashMap<String, ValueList>();
 
 		if (!po.isCheckable)
 		{
-			return new Results(null, union, 0);
+			return new StrategyResults();
 		}
 
 		INExpression exp = getINExpression(po);
 		List<INBindingSetter> binds = getINBindList(exp);
 		long before = System.currentTimeMillis();
 		IterableContext ictxt = addTypeParams(po, Interpreter.getInstance().getInitialContext());
+		boolean hasAllValues = false;
 
 		while (ictxt.hasNext())
 		{
 			ictxt.next();
 
 			for (QCStrategy strategy: strategies)
 			{
-				Results sresults = strategy.getValues(po, exp, binds, ictxt);
+				StrategyResults sresults = strategy.getValues(po, exp, binds, ictxt);
 				Map<String, ValueList> cexamples = sresults.counterexamples;
 
+				if (sresults.provedBy != null)	// No need to go further
+				{
+					return new StrategyResults(sresults.provedBy, sresults.hasAllValues, cexamples, System.currentTimeMillis() - before);
+				}
+
 				for (String bind: cexamples.keySet())
 				{
 					if (union.containsKey(bind))
@@ -343,10 +349,7 @@ public Results getValues(ProofObligation po)
 					}
 				}
 
-				if (sresults.provedBy != null)	// No need to go further
-				{
-					return new Results(sresults.provedBy, cexamples, System.currentTimeMillis() - before);
-				}
+				hasAllValues = hasAllValues || sresults.hasAllValues;	// At least one has all values
 			}
 
 			for (INBindingSetter bind: binds)
@@ -361,10 +364,10 @@ public Results getValues(ProofObligation po)
 			}
 		}
 
-		return new Results(null, union, System.currentTimeMillis() - before);
+		return new StrategyResults(null, hasAllValues, union, System.currentTimeMillis() - before);
 	}
 
-	public void checkObligation(ProofObligation po, Results results)
+	public void checkObligation(ProofObligation po, StrategyResults results)
 	{
 		try
 		{
@@ -410,9 +413,6 @@ else if (results.provedBy != null)
 					}
 				}
 
-				long before = System.currentTimeMillis();
-				Value result = new BooleanValue(false);
-				ContextException exception = null;
 				Context ctxt = Interpreter.getInstance().getInitialContext();
 
 				if (Settings.dialect != Dialect.VDM_SL)
@@ -429,6 +429,9 @@ else if (results.provedBy != null)
 				}
 
 				IterableContext ictxt = addTypeParams(po, ctxt);
+				Value execResult = new BooleanValue(false);
+				ContextException exception = null;
+				long before = System.currentTimeMillis();
 
 				try
 				{
@@ -437,42 +440,46 @@ else if (results.provedBy != null)
 					do
 					{
 						ictxt.next();
-						result = poexp.eval(ictxt);
+						execResult = poexp.eval(ictxt);
 					}
-					while (ictxt.hasNext() && result.boolValue(ctxt));
+					while (ictxt.hasNext() && execResult.boolValue(ctxt));
 				}
 				catch (ContextException e)
 				{
 					if (e.rawMessage.equals("Execution cancelled"))
 					{
-						result = null;
+						execResult = null;
 					}
 					else
 					{
-						result = new BooleanValue(false);
+						execResult = new BooleanValue(false);
 						exception = e;
 					}
 				}
 
 				long after = System.currentTimeMillis() + results.duration;
 
-				if (result == null)		// cancelled
+				if (execResult == null)		// cancelled
 				{
 					println("----");
 					printBindings(bindings);
 					println("----");
 					println(po);
 				}
-				else if (result instanceof BooleanValue)
+				else if (execResult instanceof BooleanValue)
 				{
-					if (result.boolValue(ctxt))
+					if (execResult.boolValue(ctxt))
 					{
 						POStatus outcome = null;
 
 						if (po.getCheckedExpression() instanceof TCExistsExpression)
 						{
 							outcome = POStatus.PROVED;		// An "exists" PO is PROVED, if true.
 						}
+						else if (results.hasAllValues)
+						{
+							outcome = POStatus.PROVED;		// All values were tested and passed, so PROVED
+						}
 						else
 						{
 							outcome = POStatus.MAYBE;
@@ -508,7 +515,7 @@ else if (result instanceof BooleanValue)
 				}
 				else
 				{
-					String msg = String.format("Error: PO evaluation returns %s?\n", result.kind());
+					String msg = String.format("Error: PO evaluation returns %s?\n", execResult.kind());
 					printf("PO #%d, %s\n", po.number, msg);
 					po.setStatus(POStatus.FAILED);
 					po.setCounterMessage(msg);
@@ -543,7 +550,6 @@ else if (result instanceof BooleanValue)
 		{
 			errorCount++;
 			println(e);
-			return;
 		}
 	}
 

examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckCommand.java

@@ -40,7 +40,7 @@
 
 import quickcheck.QuickCheck;
 import quickcheck.strategies.QCStrategy;
-import quickcheck.strategies.Results;
+import quickcheck.strategies.StrategyResults;
 
 public class QuickCheckCommand extends AnalysisCommand
 {
@@ -141,7 +141,7 @@ public String run(String line)
 		{
 			for (ProofObligation po: chosen)
 			{
-				Results results = qc.getValues(po);
+				StrategyResults results = qc.getValues(po);
 
 				if (!qc.hasErrors())
 				{

examples/quickcheck/src/main/java/quickcheck/commands/QuickCheckExecutor.java

@@ -36,7 +36,7 @@
 import json.JSONObject;
 import lsp.LSPServer;
 import quickcheck.QuickCheck;
-import quickcheck.strategies.Results;
+import quickcheck.strategies.StrategyResults;
 import rpc.RPCRequest;
 import workspace.PluginRegistry;
 import workspace.plugins.POPlugin;
@@ -77,7 +77,7 @@ protected void exec() throws Exception
 		{
 			for (ProofObligation po: chosen)
 			{
-				Results results = qc.getValues(po);
+				StrategyResults results = qc.getValues(po);
 
 				if (!qc.hasErrors())
 				{

examples/quickcheck/src/main/java/quickcheck/strategies/FiniteQCStrategy.java

@@ -121,11 +121,10 @@ public boolean init(QuickCheck qc)
 	}
 
 	@Override
-	public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds, Context ctxt)
+	public StrategyResults getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds, Context ctxt)
 	{
 		HashMap<String, ValueList> result = new HashMap<String, ValueList>();
 		long before = System.currentTimeMillis();
-		boolean proved = false;
 
 		if (po.isCheckable)
 		{
@@ -140,29 +139,27 @@ public Results getValues(ProofObligation po, INExpression exp, List<INBindingSet
 
 			   		if (product > expansionLimit)
 					{
-			   			return new Results(null, result, 0);	// Too big
+			   			return new StrategyResults();	// Too big
 					}
 				}
 				catch (InternalException e)		// Infinite
 				{
-					return new Results(null, result, 0);
+					return new StrategyResults();
 				}
 				catch (ArithmeticException e)	// Overflow probably
 				{
-					return new Results(null, result, 0);
+					return new StrategyResults();
 				}
 			}
 
-			// Game on...
+			// Game on... all binds can be expanded
 			for (INBindingSetter bind: binds)
 			{
 				result.put(bind.toString(), bind.getType().apply(new INGetAllValuesVisitor(), ctxt));
 			}
-
-			proved = (po.typeParams == null);	// ie. counterexamples pass and not polymorphic, then PROVED
 		}
 
-		return new Results(proved ? getName() : null, result, System.currentTimeMillis() - before);
+		return new StrategyResults(null, true, result, System.currentTimeMillis() - before);
 	}
 
 	@Override

examples/quickcheck/src/main/java/quickcheck/strategies/FixedQCStrategy.java

@@ -519,7 +519,7 @@ public boolean init(QuickCheck qc)
 	}
 
 	@Override
-	public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds, Context ctxt)
+	public StrategyResults getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds, Context ctxt)
 	{
 		Map<String, ValueList> values = new HashMap<String, ValueList>();
 		long before = System.currentTimeMillis();
@@ -542,7 +542,7 @@ public Results getValues(ProofObligation po, INExpression exp, List<INBindingSet
 			println(e);
 		}
 
-		return new Results(null, values, System.currentTimeMillis() - before);
+		return new StrategyResults(null, false, values, System.currentTimeMillis() - before);
 	}
 
 	@Override

examples/quickcheck/src/main/java/quickcheck/strategies/QCStrategy.java

@@ -39,6 +39,6 @@ abstract public class QCStrategy
 	abstract public boolean hasErrors();
 	abstract public boolean useByDefault();
 	abstract public boolean init(QuickCheck qc);
-	abstract public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds, Context ctxt);
+	abstract public StrategyResults getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds, Context ctxt);
 	abstract public String help();
 }

examples/quickcheck/src/main/java/quickcheck/strategies/RandomQCStrategy.java

@@ -127,7 +127,7 @@ public boolean init(QuickCheck qc)
 	}
 
 	@Override
-	public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds, Context ctxt)
+	public StrategyResults getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds, Context ctxt)
 	{
 		HashMap<String, ValueList> result = new HashMap<String, ValueList>();
 		long before = System.currentTimeMillis();
@@ -144,7 +144,7 @@ public Results getValues(ProofObligation po, INExpression exp, List<INBindingSet
 			}
 		}
 
-		return new Results(null, result, System.currentTimeMillis() - before);
+		return new StrategyResults(null, false, result, System.currentTimeMillis() - before);
 	}
 
 	@Override

examples/quickcheck/src/main/java/quickcheck/strategies/SearchQCStrategy.java

@@ -83,7 +83,7 @@ public boolean init(QuickCheck qc)
 	}
 
 	@Override
-	public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds, Context ctxt)
+	public StrategyResults getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds, Context ctxt)
 	{
 		HashMap<String, ValueList> result = new HashMap<String, ValueList>();
 		long before = System.currentTimeMillis();
@@ -134,7 +134,7 @@ public Results getValues(ProofObligation po, INExpression exp, List<INBindingSet
 			}
 		}
 
-		return new Results(null, result, System.currentTimeMillis() - before);
+		return new StrategyResults(null, false, result, System.currentTimeMillis() - before);
 	}
 
 	@Override

examples/quickcheck/src/main/java/quickcheck/strategies/Results.java → examples/quickcheck/src/main/java/quickcheck/strategies/StrategyResults.java

@@ -24,24 +24,38 @@
 
 package quickcheck.strategies;
 
+import java.util.HashMap;
 import java.util.Map;
 
 import com.fujitsu.vdmj.values.ValueList;
 
 /**
  * A class to hold the return values of a getValues() call on a QC plugin.
  * The provedBy field indicates that the PO has been proved to have no counterexamples.
- * Otherwise, counterexamples contains known or possible values to check.
+ * Otherwise, counterexamples contains known or possible values to check. The
+ * hasAllValues field indicates that all possible values of all bindings are included
+ * (probably from the "finite" strategy) and hence if no counterexamples are found,
+ * the PO is proved.
  */
-public class Results
+public class StrategyResults
 {
-	public final String provedBy;
+	public final String provedBy;			// If set, proved already
+	public final boolean hasAllValues;		// Contains all possible values from all binds
 	public final Map<String, ValueList> counterexamples;
-	public final long duration;		// time to generate counterexamples, in millisecs
-
-	public Results(String proved, Map<String, ValueList> counterexamples, long duration)
+	public final long duration;				// time to generate counterexamples, in millisecs
+
+	public StrategyResults()
+	{
+		this.provedBy = null;
+		this.hasAllValues = false;
+		this.counterexamples = new HashMap<String, ValueList>();
+		this.duration = 0;
+	}
+
+	public StrategyResults(String proved, boolean hasAllValues, Map<String, ValueList> counterexamples, long duration)
 	{
 		this.provedBy = proved;
+		this.hasAllValues = hasAllValues;
 		this.counterexamples = counterexamples;
 		this.duration = duration;
 	}

examples/quickcheck/src/main/java/quickcheck/strategies/TrivialQCStrategy.java

@@ -79,18 +79,21 @@ public boolean init(QuickCheck qc)
 	}
 
 	@Override
-	public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds, Context ctxt)
+	public StrategyResults getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds, Context ctxt)
 	{
 		long before = System.currentTimeMillis();
-		boolean proved = false;
+		String provedBy = null;
 
 		if (po.isCheckable && po.getCheckedExpression() != null)
 		{
 			TrivialQCVisitor visitor = new TrivialQCVisitor();
-			proved = po.getCheckedExpression().apply(visitor, new Stack<TCExpression>());
+			if (po.getCheckedExpression().apply(visitor, new Stack<TCExpression>()))
+			{
+				provedBy = getName();
+			}
 		}
 
-		return new Results(proved ? getName() : null, new HashMap<String, ValueList>(), System.currentTimeMillis() - before);
+		return new StrategyResults(provedBy, false, new HashMap<String, ValueList>(), System.currentTimeMillis() - before);
 	}
 
 	@Override