Merge branch 'master' into highprecision

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

@@ -0,0 +1,107 @@
+/*******************************************************************************
+ *
+ *	Copyright (c) 2023 Nick Battle.
+ *
+ *	Author: Nick Battle
+ *
+ *	This file is part of VDMJ.
+ *
+ *	VDMJ is free software: you can redistribute it and/or modify
+ *	it under the terms of the GNU General Public License as published by
+ *	the Free Software Foundation, either version 3 of the License, or
+ *	(at your option) any later version.
+ *
+ *	VDMJ is distributed in the hope that it will be useful,
+ *	but WITHOUT ANY WARRANTY; without even the implied warranty of
+ *	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ *	GNU General Public License for more details.
+ *
+ *	You should have received a copy of the GNU General Public License
+ *	along with VDMJ.  If not, see <http://www.gnu.org/licenses/>.
+ *	SPDX-License-Identifier: GPL-3.0-or-later
+ *
+ ******************************************************************************/
+
+package quickcheck.strategies;
+
+import static com.fujitsu.vdmj.plugins.PluginConsole.errorln;
+
+import java.util.HashMap;
+import java.util.List;
+import java.util.Stack;
+
+import com.fujitsu.vdmj.in.expressions.INExpression;
+import com.fujitsu.vdmj.in.patterns.INBindingSetter;
+import com.fujitsu.vdmj.pog.ProofObligation;
+import com.fujitsu.vdmj.runtime.Context;
+import com.fujitsu.vdmj.tc.expressions.TCExpression;
+import com.fujitsu.vdmj.values.ValueList;
+
+import quickcheck.QuickCheck;
+import quickcheck.visitors.TrivialQCVisitor;
+
+public class TrivialQCStrategy extends QCStrategy
+{
+	private int errorCount = 0;
+
+	public TrivialQCStrategy(List<String> argv)
+	{
+		for (int i=0; i < argv.size(); i++)
+		{
+			// No plugin arguments yet?
+
+			if (argv.get(i).startsWith("-trivial:"))
+			{
+				errorln("Unknown trivial option: " + argv.get(i));
+				errorln(help());
+				errorCount ++;
+				argv.remove(i);
+			}
+		}
+	}
+
+	@Override
+	public String getName()
+	{
+		return "trivial";
+	}
+
+	@Override
+	public boolean hasErrors()
+	{
+		return errorCount > 0;
+	}
+
+	@Override
+	public boolean init(QuickCheck qc)
+	{
+		return true;
+	}
+
+	@Override
+	public Results getValues(ProofObligation po, INExpression exp, List<INBindingSetter> binds, Context ctxt)
+	{
+		long before = System.currentTimeMillis();
+		boolean proved = false;
+
+		if (po.isCheckable && po.getCheckedExpression() != null)
+		{
+			TrivialQCVisitor visitor = new TrivialQCVisitor();
+			proved = po.getCheckedExpression().apply(visitor, new Stack<TCExpression>());
+		}
+
+		return new Results(proved, new HashMap<String, ValueList>(), System.currentTimeMillis() - before);
+	}
+
+	@Override
+	public String help()
+	{
+		return getName() + " (no options)";
+	}
+
+	@Override
+	public boolean useByDefault()
+	{
+		return true;	// Use if no -s given
+	}
+}

examples/quickcheck/src/main/java/quickcheck/visitors/TrivialQCVisitor.java

@@ -0,0 +1,182 @@
+/*******************************************************************************
+ *
+ *	Copyright (c) 2023 Nick Battle.
+ *
+ *	Author: Nick Battle
+ *
+ *	This file is part of VDMJ.
+ *
+ *	VDMJ is free software: you can redistribute it and/or modify
+ *	it under the terms of the GNU General Public License as published by
+ *	the Free Software Foundation, either version 3 of the License, or
+ *	(at your option) any later version.
+ *
+ *	VDMJ is distributed in the hope that it will be useful,
+ *	but WITHOUT ANY WARRANTY; without even the implied warranty of
+ *	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ *	GNU General Public License for more details.
+ *
+ *	You should have received a copy of the GNU General Public License
+ *	along with VDMJ.  If not, see <http://www.gnu.org/licenses/>.
+ *	SPDX-License-Identifier: GPL-3.0-or-later
+ *
+ ******************************************************************************/
+
+package quickcheck.visitors;
+
+import java.util.Stack;
+
+import com.fujitsu.vdmj.ast.lex.LexKeywordToken;
+import com.fujitsu.vdmj.lex.Token;
+import com.fujitsu.vdmj.tc.expressions.TCEqualsExpression;
+import com.fujitsu.vdmj.tc.expressions.TCExpression;
+import com.fujitsu.vdmj.tc.expressions.TCForAllExpression;
+import com.fujitsu.vdmj.tc.expressions.TCIfExpression;
+import com.fujitsu.vdmj.tc.expressions.TCImpliesExpression;
+import com.fujitsu.vdmj.tc.expressions.TCInSetExpression;
+import com.fujitsu.vdmj.tc.expressions.TCIntegerLiteralExpression;
+import com.fujitsu.vdmj.tc.expressions.TCMapEnumExpression;
+import com.fujitsu.vdmj.tc.expressions.TCNotEqualExpression;
+import com.fujitsu.vdmj.tc.expressions.TCNotExpression;
+import com.fujitsu.vdmj.tc.expressions.TCSeqEnumExpression;
+import com.fujitsu.vdmj.tc.expressions.TCSetEnumExpression;
+import com.fujitsu.vdmj.tc.expressions.TCVariableExpression;
+import com.fujitsu.vdmj.tc.expressions.visitors.TCExpressionVisitor;
+import com.fujitsu.vdmj.tc.patterns.TCIdentifierPattern;
+import com.fujitsu.vdmj.tc.patterns.TCMultipleBind;
+import com.fujitsu.vdmj.tc.patterns.TCMultipleSetBind;
+import com.fujitsu.vdmj.tc.patterns.TCPattern;
+
+/**
+ * Search for trivial truths in POs. Each method is passed a stack of expressions
+ * which are known to be true in the current context and they return true if they
+ * are always true, given this stack.
+ * 
+ * eg. X => Y will pass "X" as a truth when evaluating Y. If Y is just X, then
+ * that will always be true and so the whole implication is always true, etc.
+ */
+public class TrivialQCVisitor extends TCExpressionVisitor<Boolean, Stack<TCExpression>>
+{
+	public TrivialQCVisitor()
+	{
+	}
+
+	@Override
+	public Boolean caseForAllExpression(TCForAllExpression node, Stack<TCExpression> truths)
+	{
+		int pushes = 0;
+
+		for (TCMultipleBind bind: node.bindList)
+		{
+			if (bind instanceof TCMultipleSetBind)
+			{
+				TCMultipleSetBind sbind = (TCMultipleSetBind)bind;
+
+				for (TCPattern p: sbind.plist)
+				{
+					if (p instanceof TCIdentifierPattern)
+					{
+						TCIdentifierPattern id = (TCIdentifierPattern)p;
+
+						truths.push(new TCInSetExpression(
+							new TCVariableExpression(id.location, id.name, p.toString()),
+							new LexKeywordToken(Token.INSET, sbind.location),
+							sbind.set));
+
+						pushes++;	// eg. "x in set S" is always true here
+					}
+				}
+			}
+		}
+
+		boolean result = node.predicate.apply(this, truths);
+
+		for (int i=0; i<pushes; i++)
+		{
+			truths.pop();
+		}
+
+		return result;
+	}
+
+	@Override
+	public Boolean caseIfExpression(TCIfExpression node, Stack<TCExpression> truths)
+	{
+		truths.push(node.ifExp);
+		boolean result1 = node.thenExp.apply(this, truths);
+		truths.pop();
+
+		truths.push(new TCNotExpression(node.location, node.ifExp));
+		boolean result2 = node.elseExp.apply(this, truths);
+		truths.pop();
+
+		return result1 && result2;		// All paths always true
+	}
+
+	@Override
+	public Boolean caseImpliesExpression(TCImpliesExpression node, Stack<TCExpression> truths)
+	{
+		truths.push(node.left);
+
+		if (node.left instanceof TCEqualsExpression)
+		{
+			TCEqualsExpression eq = (TCEqualsExpression)node.left;
+			truths.push(new TCNotEqualExpression(eq.left, new LexKeywordToken(Token.NE, eq.location), eq.right));
+		}
+
+		boolean result = node.right.apply(this, truths);
+
+		if (node.left instanceof TCEqualsExpression)
+		{
+			truths.pop();
+		}
+
+		truths.pop();
+		return result;
+	}
+
+	@Override
+	public Boolean caseNotEqualExpression(TCNotEqualExpression node, Stack<TCExpression> truths)
+	{
+		if (node.left instanceof TCSeqEnumExpression &&
+			node.right instanceof TCSeqEnumExpression)
+		{
+			TCSeqEnumExpression sleft = (TCSeqEnumExpression)node.left;
+			TCSeqEnumExpression sright = (TCSeqEnumExpression)node.right;
+
+			return (sleft.members.isEmpty() != sright.members.isEmpty());	// eg. [1,2,3] <> []
+		}
+		else if (node.left instanceof TCSetEnumExpression &&
+			node.right instanceof TCSetEnumExpression)
+		{
+			TCSetEnumExpression sleft = (TCSetEnumExpression)node.left;
+			TCSetEnumExpression sright = (TCSetEnumExpression)node.right;
+
+			return (sleft.members.isEmpty() != sright.members.isEmpty());	// eg. {1,2,3} <> {}
+		}
+		else if (node.left instanceof TCMapEnumExpression &&
+			node.right instanceof TCMapEnumExpression)
+		{
+			TCMapEnumExpression sleft = (TCMapEnumExpression)node.left;
+			TCMapEnumExpression sright = (TCMapEnumExpression)node.right;
+
+			return (sleft.members.isEmpty() != sright.members.isEmpty());	// eg. {1|->2} <> {|->}
+		}
+		else if (node.left instanceof TCIntegerLiteralExpression &&
+			node.right instanceof TCIntegerLiteralExpression)
+		{
+			TCIntegerLiteralExpression vleft = (TCIntegerLiteralExpression)node.left;
+			TCIntegerLiteralExpression vright = (TCIntegerLiteralExpression)node.right;
+
+			return (vleft.value.value != vright.value.value);		// eg. 123 <> 456
+		}
+
+		return false;
+	}
+
+	@Override
+	public Boolean caseExpression(TCExpression node, Stack<TCExpression> truths)
+	{
+		return truths.contains(node);
+	}
+}

examples/quickcheck/src/main/resources/qc.strategies

@@ -1,4 +1,5 @@
 quickcheck.strategies.FixedQCStrategy
 quickcheck.strategies.SearchQCStrategy
 quickcheck.strategies.RandomQCStrategy
-quickcheck.strategies.FiniteQCStrategy
+quickcheck.strategies.FiniteQCStrategy
+quickcheck.strategies.TrivialQCStrategy