Created
October 10, 2017 11:20
-
-
Save rindPHI/70b9a4b2ee3159f4f55f59ea2198637a to your computer and use it in GitHub Desktop.
Programmatically using KeY as a program verifier.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
package example; | |
import java.io.File; | |
import java.util.HashMap; | |
import java.util.LinkedList; | |
import java.util.List; | |
import java.util.Set; | |
import org.key_project.util.collection.ImmutableSet; | |
import de.uka.ilkd.key.control.KeYEnvironment; | |
import de.uka.ilkd.key.java.abstraction.KeYJavaType; | |
import de.uka.ilkd.key.logic.op.IObserverFunction; | |
import de.uka.ilkd.key.proof.Proof; | |
import de.uka.ilkd.key.proof.init.ProofInputException; | |
import de.uka.ilkd.key.proof.io.ProblemLoaderException; | |
import de.uka.ilkd.key.settings.ChoiceSettings; | |
import de.uka.ilkd.key.settings.ProofSettings; | |
import de.uka.ilkd.key.speclang.Contract; | |
import de.uka.ilkd.key.strategy.StrategyProperties; | |
import de.uka.ilkd.key.util.KeYTypeUtil; | |
import de.uka.ilkd.key.util.MiscTools; | |
/** | |
* Example application which proves all proof obligations of | |
* the source folder 'example' using KeY. | |
* @author Martin Hentschel | |
*/ | |
public class Main { | |
/** | |
* The program entry point. | |
* @param args The start parameters. | |
*/ | |
public static void main(String[] args) { | |
File location = args.length == 1 ? | |
new File(args[0]) : | |
new File("example"); // Path to the source code folder/file or to a *.proof file | |
List<File> classPaths = null; // Optionally: Additional specifications for API classes | |
File bootClassPath = null; // Optionally: Different default specifications for Java API | |
List<File> includes = null; // Optionally: Additional includes to consider | |
try { | |
// Ensure that Taclets are parsed | |
if (!ProofSettings.isChoiceSettingInitialised()) { | |
KeYEnvironment<?> env = KeYEnvironment.load(location, classPaths, bootClassPath, includes); | |
env.dispose(); | |
} | |
// Set Taclet options | |
ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings(); | |
HashMap<String, String> oldSettings = choiceSettings.getDefaultChoices(); | |
HashMap<String, String> newSettings = new HashMap<String, String>(oldSettings); | |
newSettings.putAll(MiscTools.getDefaultTacletOptions()); | |
choiceSettings.setDefaultChoices(newSettings); | |
// Load source code | |
KeYEnvironment<?> env = KeYEnvironment.load(location, classPaths, bootClassPath, includes); | |
// env.getLoadedProof() returns the performed proof if a *.proof file is loaded | |
try { | |
// List all specifications of all types in the source location (not classPaths and bootClassPath) | |
final List<Contract> proofContracts = new LinkedList<Contract>(); | |
Set<KeYJavaType> kjts = env.getJavaInfo().getAllKeYJavaTypes(); | |
for (KeYJavaType type : kjts) { | |
if (!KeYTypeUtil.isLibraryClass(type)) { | |
ImmutableSet<IObserverFunction> targets = env.getSpecificationRepository().getContractTargets(type); | |
for (IObserverFunction target : targets) { | |
ImmutableSet<Contract> contracts = env.getSpecificationRepository().getContracts(type, target); | |
for (Contract contract : contracts) { | |
proofContracts.add(contract); | |
} | |
} | |
} | |
} | |
// Perform proofs | |
for (Contract contract : proofContracts) { | |
Proof proof = null; | |
try { | |
// Create proof | |
proof = env.createProof(contract.createProofObl(env.getInitConfig(), contract)); | |
// Set proof strategy options | |
StrategyProperties sp = proof.getSettings().getStrategySettings().getActiveStrategyProperties(); | |
sp.setProperty(StrategyProperties.METHOD_OPTIONS_KEY, StrategyProperties.METHOD_CONTRACT); | |
sp.setProperty(StrategyProperties.DEP_OPTIONS_KEY, StrategyProperties.DEP_ON); | |
sp.setProperty(StrategyProperties.QUERY_OPTIONS_KEY, StrategyProperties.QUERY_ON); | |
sp.setProperty(StrategyProperties.NON_LIN_ARITH_OPTIONS_KEY, StrategyProperties.NON_LIN_ARITH_DEF_OPS); | |
sp.setProperty(StrategyProperties.STOPMODE_OPTIONS_KEY, StrategyProperties.STOPMODE_NONCLOSE); | |
proof.getSettings().getStrategySettings().setActiveStrategyProperties(sp); | |
// Make sure that the new options are used | |
int maxSteps = 10000; | |
ProofSettings.DEFAULT_SETTINGS.getStrategySettings().setMaxSteps(maxSteps); | |
ProofSettings.DEFAULT_SETTINGS.getStrategySettings().setActiveStrategyProperties(sp); | |
proof.getSettings().getStrategySettings().setMaxSteps(maxSteps); | |
proof.setActiveStrategy(proof.getServices().getProfile().getDefaultStrategyFactory().create(proof, sp)); | |
// Start auto mode | |
env.getUi().getProofControl().startAndWaitForAutoMode(proof); | |
// Show proof result | |
boolean closed = proof.openGoals().isEmpty(); | |
System.out.println("Contract '" + contract.getDisplayName() + "' of " + contract.getTarget() + " is " + (closed ? "verified" : "still open") + "."); | |
} | |
catch (ProofInputException e) { | |
System.out.println("Exception at '" + contract.getDisplayName() + "' of " + contract.getTarget() + ":"); | |
e.printStackTrace(); | |
} | |
finally { | |
if (proof != null) { | |
proof.dispose(); // Ensure always that all instances of Proof are disposed | |
} | |
} | |
} | |
} | |
finally { | |
env.dispose(); // Ensure always that all instances of KeYEnvironment are disposed | |
} | |
} | |
catch (ProblemLoaderException e) { | |
System.out.println("Exception at '" + location + "':"); | |
e.printStackTrace(); | |
} | |
} | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment