Implement a PVS expression generator. (c0a04f53) · Commits · tables / jtet

src/main/java/ca/mcscert/jtet/pvsgenerator/PVSExpressionGenerator.java

0 → 100644

+130 −0

Original line number	Diff line number	Diff line
		/*
		* Copyright (C) 2014 Matthew Dawson <matthew@mjdsystems.ca>
		*
		* Redistribution and use in source and binary forms, with or without
		* modification, are permitted provided that the following conditions are
		* met:
		*
		* * Redistributions of source code must retain the above copyright
		* notice, this list of conditions and the following disclaimer.
		* * Redistributions in binary form must reproduce the above copyright
		* notice, this list of conditions and the following disclaimer in
		* the documentation and/or other materials provided with the distribution
		* * Neither the name of the McMaster Centre for Software Certification nor the names
		* of its contributors may be used to endorse or promote products derived
		* from this software without specific prior written permission.
		*
		* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
		* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
		* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
		* ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
		* LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
		* CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
		* SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
		* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
		* CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
		* ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
		* POSSIBILITY OF SUCH DAMAGE.
		*/

		package ca.mcscert.jtet.pvsgenerator;

		import ca.mcscert.jtet.expression.*;

		/** Generates PVS expressions.
		* <p>
		* Provides an implementation of {@link ca.mcscert.jtet.expression.ExpressionGenerator} for PVS.
		* @author Matthew Dawson
		*/
		public class PVSExpressionGenerator implements ExpressionGenerator {
		/**
		* Provides a static PVSExpressionGenerator for use.
		* <p>
		* Since PVSExpressionGenerator is thread-safe, this avoid an allocation before use.
		*/
		public final static PVSExpressionGenerator Generator = new PVSExpressionGenerator();

		/**
		* Converts binary operators to PVS specific syntax.
		* @param op Operator to convert
		* @return PVS syntax
		* @throws java.lang.IllegalArgumentException If PVS does not support specified operator.
		*/
		private static String GetInfixSymbolFor(BinaryOperation op) {
		switch (op) {
		case Addition:
		return "+";
		case Minus:
		return "-";
		case Multiplication:
		return "*";
		case Division:
		return "/";
		case Exponentiation:
		return "^";
		case GreaterThen:
		return ">";
		case GreaterThenEqual:
		return ">=";
		case LessThen:
		return "<";
		case LessThenEqual:
		return "<=";
		case Equals:
		return "=";
		case NotEquals:
		return "/=";
		case BooleanAnd:
		return "AND";
		case BooleanOr:
		return "OR";
		case Implies:
		return "=>";
		}
		throw new IllegalArgumentException("Should never happen!");
		}

		/**
		* {@inheritDoc}
		*/
		@Override
		public String GenerateBinaryOperation(BinaryOperation op, String lhsExp, String rhsExp, Type usedType) {
		return "(" + lhsExp + " " + GetInfixSymbolFor(op) + " " + rhsExp + ")";
		}

		/**
		* Converts unary operators to PVS specific syntax.
		* @param op Operator to convert
		* @return PVS syntax
		* @throws java.lang.IllegalArgumentException If PVS does not support specified operator.
		*/
		private static String GetUnaryOperationSymbolFor(UnaryOperation op) {
		switch (op) {
		case Negation:
		return "NOT";
		case Minus:
		return "-";
		}
		throw new IllegalArgumentException("Should never happen! Asked for unhandled op: " + op + "!");
		}

		/**
		* {@inheritDoc}
		*/
		@Override
		public String GenerateUnaryOperation(UnaryOperation op, String expression, Type usedType) {
		return "(" + GetUnaryOperationSymbolFor(op) + " " + expression + ")";
		}

		/**
		* {@inheritDoc}
		*/
		@Override
		public String GenerateLiteralValue(String value, Type requestedType) {
		if (requestedType instanceof RealType) {
		return value;
		} else {
		throw new IllegalArgumentException("Can't cast literal to that type!");
		}
		}
		}

src/test/java/ca/mcscert/jtet/expression/GenericOperationGeneratorTest.java

+6 −0

Original line number	Diff line number	Diff line
		@@ -34,6 +34,7 @@ import ca.mcscert.jtet.salgenerator.SALExpressionGenerator;
		import ca.mcscert.jtet.smtlibchecker.SMTLIBExpressionGenerator;
		import ca.mcscert.jtet.parsers.PVSSimpleParser;
		import ca.mcscert.jtet.parsers.VariableParser;
		import ca.mcscert.jtet.pvsgenerator.PVSExpressionGenerator;
		import org.junit.Test;
		import org.junit.runner.RunWith;
		import org.junit.runners.Parameterized;
		@@ -72,6 +73,11 @@ public class GenericOperationGeneratorTest {
		null,
		null
		},
		{new PVSExpressionGenerator(),
		"((((x * 5) = (1 / (- 4))) OR (((x > (8 + 3)) AND (9 < (x - 2))) OR ((x >= 12) OR ((NOT (34 <= (- x))) OR (5 > 4))))) => (x /= 5))",
		null,
		null
		},
		{new ExpressionGeneratorSpy(new CVC3ExpressionGenerator()),
		"((((x * 5) = (1 / (- 4))) OR (((x > (8 + 3)) AND (9 < (x - 2))) OR ((x >= 12) OR ((NOT (34 <= (- x))) OR (5 > 4))))) => (x /= 5))",
		"(((BVMULT(8,x,0bin00010100) = BVSDIV(0bin00000100,BVUMINUS(0bin00010000))) OR ((BVSGT(x,BVPLUS(8,0bin00100000,0bin00001100)) AND BVSLT(0bin00100100,BVSUB(8,x,0bin00001000))) OR (BVSGE(x,0bin00110000) OR ((NOT BVSLE(0bin10001000,BVUMINUS(x))) OR (5 > 4))))) => (x /= 0bin00010100))",