Implement variable declaration generation for PVS. (743f3096) · Commits · tables / jtet

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

0 → 100644

+101 −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.*;

		import java.util.Collection;

		/**
		* Generates variable declarations for PVS, for use by {@link ca.mcscert.jtet.pvsgenerator.PVSTableGenerator}
		* <p>
		* * Provides an implementation of {@link ca.mcscert.jtet.expression.VariablesDeclarationGenerator} for PVS.
		* @author Matthew Dawson
		*/
		public class PVSVariableDeclarationGenerator implements VariablesDeclarationGenerator {
		/**
		* Generate the PVS specific name for variable types.
		* @param type The type to get the name for.
		* @return PVS name for the given type.
		* @throws java.lang.IllegalArgumentException If the given type cannot be represented by PVS.
		*/
		private String GenerateVariableType(Type type) {
		if (type instanceof RealType) {
		return "real";
		} else if (type instanceof BooleanType) {
		return "bool";
		} else {
		throw new IllegalArgumentException("The PVS Generator doesn't currently handle this variable type (Class: " + type.getClass().getName() + ")");
		}
		}

		@Override
		public String GenerateVariablesDeclaration(Collection<Variable> variables) {
		StringBuilder ret = new StringBuilder();

		boolean isFirst = true;
		// Generate all the variables.
		for(Variable var : variables) {
		if (!isFirst) {
		ret.append(",");
		}
		ret.append(var.outputName()).append(":");
		generateVariableTypeInformation(ret, var);
		isFirst = false;
		}

		return ret.toString();
		}

		/**
		* Generates the typing information for a given variable.
		* <p>
		* This is a helper used by {@link #GenerateVariablesDeclaration(java.util.Collection)} to generate the type information
		* for a given variable. This is broken out to a separate function so that
		* {@link ca.mcscert.jtet.pvsgenerator.PVSTableGenerator} can call it for the single output variable case, and should
		* otherwise not be called externally.
		* @param output The StringBuilder to append the output to.
		* @param variable The variable to generate the typing information for.
		*/
		void generateVariableTypeInformation(StringBuilder output, Variable variable) {
		Type type = variable.type();
		if (variable.subtypePredicate() == null) {
		output.append(GenerateVariableType(type));
		} else {
		output.append("{")
		.append(variable.outputName())
		.append(":")
		.append(GenerateVariableType(type))
		.append("\|")
		.append(variable.subtypePredicate().getCheckerOutput(PVSExpressionGenerator.Generator, BooleanType.Type))
		.append("}");
		}
		}
		}

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

+12 −0

Original line number	Diff line number	Diff line
		@@ -31,6 +31,7 @@ package ca.mcscert.jtet.expression;
		import ca.mcscert.jtet.cvc3generator.CVC3VariablesDeclarationGenerator;
		import ca.mcscert.jtet.eventbgenerator.EventBVariablesDeclarationGenerator;
		import ca.mcscert.jtet.parsers.VariableParser;
		import ca.mcscert.jtet.pvsgenerator.PVSVariableDeclarationGenerator;
		import ca.mcscert.jtet.salgenerator.SALVariablesDeclarationGenerator;
		import ca.mcscert.jtet.smtlibchecker.SMTLIBVariablesDeclarationGenerator;
		import org.junit.Before;
		@@ -109,6 +110,17 @@ public class GenericVariablesDeclarationGeneratorTest {
		null,
		null
		},
		{new PVSVariableDeclarationGenerator(),
		"x:real",
		"new_x_name:real",
		"x:{x:real\|(x > 0)}",
		"x:bool",
		null,
		null,
		null,
		null,
		null
		},
		});
		}
		@Parameter(value = 0)