@@ -0,0 +1,2687 @@
+package edu.kit.iti.formal.pse.worthwhile.prover;%0A%0Aimport java.util.HashMap;%0Aimport java.util.Map;%0A%0Aimport org.junit.Assert;%0Aimport org.junit.Before;%0Aimport org.junit.Test;%0A%0Aimport edu.kit.iti.formal.pse.worthwhile.common.tests.TestASTProvider;%0Aimport edu.kit.iti.formal.pse.worthwhile.model.BooleanValue;%0Aimport edu.kit.iti.formal.pse.worthwhile.model.Value;%0Aimport edu.kit.iti.formal.pse.worthwhile.model.ast.AstFactory;%0Aimport edu.kit.iti.formal.pse.worthwhile.model.ast.BooleanLiteral;%0Aimport edu.kit.iti.formal.pse.worthwhile.model.ast.Equal;%0Aimport edu.kit.iti.formal.pse.worthwhile.model.ast.Program;%0Aimport edu.kit.iti.formal.pse.worthwhile.model.ast.VariableDeclaration;%0Aimport edu.kit.iti.formal.pse.worthwhile.model.ast.VariableReference;%0A%0A/**%0A * Test the functionality of %7B@link SpecificationChecker%7D.%0A * %0A * @author Leon Handreke%0A * %0A */%0Apublic class SpecificationCheckerTest %7B%0A%0A%09/**%0A%09 * The %7B@link SpecificationChecker%7D to use.%0A%09 */%0A%09private SpecificationChecker checker;%0A%0A%09/**%0A%09 * Instantiate a new %7B@link SpecificationChecker%7D for all tests.%0A%09 */%0A%09@Before%0A%09public final void setUpSpecificationChecker() %7B%0A%09%09this.checker = new SpecificationChecker();%0A%09%7D%0A%0A%09/**%0A%09 * Test the checkExpression method by asserting an expression about an environment.%0A%09 */%0A%09@Test%0A%09public final void testEnvironmentAssertion() %7B%0A%09%09// construct a new Boolean a%0A%09%09VariableDeclaration aDeclaration = AstFactory.init().createVariableDeclaration();%0A%09%09aDeclaration.setName(%22a%22);%0A%09%09aDeclaration.setType(AstFactory.init().createBooleanType());%0A%0A%09%09// build the expression a = true%0A%09%09VariableReference aReference = AstFactory.init().createVariableReference();%0A%09%09aReference.setVariable(aDeclaration);%0A%09%09BooleanLiteral trueLiteral = AstFactory.init().createBooleanLiteral();%0A%09%09trueLiteral.setValue(true);%0A%09%09Equal equal = AstFactory.init().createEqual();%0A%09%09equal.setLeft(aReference);%0A%09%09equal.setRight(trueLiteral);%0A%0A%09%09// build an environment that has a set to true%0A%09%09Map%3CVariableDeclaration, Value%3E environment = new HashMap%3CVariableDeclaration, Value%3E();%0A%09%09Value aValue = new BooleanValue(true);%0A%09%09environment.put(aDeclaration, aValue);%0A%0A%09%09// check if the prover verifies the formula%0A%09%09Validity validity = this.checker.checkFormula(equal, environment);%0A%09%09Assert.assertEquals(Validity.VALID, validity);%0A%09%7D%0A%0A%09/**%0A%09 * Test assigning a number to an array at an index and proving that it's there.%0A%09 */%0A%09@Test%0A%09public final void testArrayIndexAssignment() %7B%0A%09%09Program p = TestASTProvider%0A%09%09                .getRootASTNode(%22Integer%5B%5D a := %7B1, 2, 3%7D%5Cna%5B0%5D := 42%5Cn_assert a%5B0%5D = 42 && a%5B1%5D = 2 && a%5B2%5D = 3%5Cn%22);%0A%09%09Validity validity = this.checker.checkProgram(p);%0A%09%09Assert.assertEquals(Validity.VALID, validity);%0A%09%7D%0A%7D%0A

Add SpecificationCheckerTest for integration tests