diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java index e5817e32ee8..a7b80ba2a62 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java @@ -203,6 +203,18 @@ private IBuiltInRuleApp constructBuiltinApp(Node originalStep, Goal currGoal) return ourApp; } + private NoPosTacletApp lookupIntroducedTaclet(TacletApp app, Goal goal) { + for (Node n = goal.node(); n != null; n = n.parent()) { + for (NoPosTacletApp introduced : n.getLocalIntroducedRules()) { + if (EqualityModuloProofIrrelevancy.equalsModProofIrrelevancy(introduced, + app)) { + return introduced; + } + } + } + return null; + } + /** * Construct a new taclet application based on a step in the original proof * @@ -228,16 +240,21 @@ private TacletApp constructTacletApp(Node originalStep, Goal currGoal) { // find the correct taclet for (NoPosTacletApp partialApp : currGoal.indexOfTaclets() .getPartialInstantiatedApps()) { - System.out.println(); if (EqualityModuloProofIrrelevancy.equalsModProofIrrelevancy(partialApp, originalTacletApp)) { ourApp = partialApp; break; } } + + if (ourApp == null) { + ourApp = lookupIntroducedTaclet(originalTacletApp, currGoal); + } + if (ourApp == null) { ourApp = currGoal.indexOfTaclets().lookup(tacletName); } + if (ourApp == null) { throw new IllegalStateException( "proof replayer failed to find dynamically added taclet at original node " diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/EqualityModuloProofIrrelevancy.java b/key.core/src/main/java/de/uka/ilkd/key/rule/EqualityModuloProofIrrelevancy.java index 73bc1013f65..2821ccf4c68 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/EqualityModuloProofIrrelevancy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/EqualityModuloProofIrrelevancy.java @@ -490,6 +490,13 @@ public static boolean equalsModProofIrrelevancy(org.key_project.prover.rules.Tac return false; } + if (_this instanceof FindTaclet _thisFind) { + final FindTaclet thatFind = (FindTaclet) that; + if (!_thisFind.find().equalsModProperty(thatFind.find(), PROOF_IRRELEVANCY_PROPERTY)) { + return false; + } + } + if ((_this.assumesSequent() == null && that.assumesSequent() != null) || (_this.assumesSequent() != null && that.assumesSequent() == null)) { return false; @@ -523,8 +530,16 @@ && equalsModProofIrrelevancy(if1.head(), if2.head())) { * @return the hash code modulo proof irrelevancy for the given argument */ public static int hashCodeModProofIrrelevancy(org.key_project.prover.rules.Taclet taclet) { - Sequent sequentFormulas = taclet.assumesSequent(); - return hashCodeModProofIrrelevancy(sequentFormulas.getFormulaByNr(1)); + int hashCode = 17; + hashCode += 17 * (taclet.getChoices().hashCode() + 17 * taclet.goalTemplates().size()); + if (taclet instanceof final FindTaclet find) { + hashCode += 17 * PROOF_IRRELEVANCY_PROPERTY.hashCodeModThisProperty(find.find()); + } + final Sequent assumesSequent = taclet.assumesSequent(); + if (assumesSequent != null && !assumesSequent.isEmpty()) { + hashCode += 17 * hashCodeModProofIrrelevancy(assumesSequent.getFormulaByNr(1)); + } + return hashCode; } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/util/Random.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/util/Random.java new file mode 100644 index 00000000000..2b3f5a37f9f --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/util/Random.java @@ -0,0 +1,96 @@ +package java.util; + +public class Random implements java.util.random.RandomGenerator, java.io.Serializable { + + // @Override + public void setSeed(long seed); + + // @Override + public boolean isDeprecated(); + + // @Override + public void nextBytes(byte[] bytes); + + // @Override + public int nextInt(); + + public int nextInt(int bound); + + // @Override + public int nextInt(int origin, int bound); + + // @Override + public long nextLong(); + // @Override + public long nextLong(long bound); + + // @Override + public long nextLong(long origin, long bound); + + // @Override + public boolean nextBoolean(); + + // @Override + public float nextFloat(); + + // @Override + public float nextFloat(float bound); + + // @Override + public float nextFloat(float origin, float bound); + + // @Override + public double nextDouble(); + + // @Override + public double nextDouble(double bound); + + // @Override + public double nextDouble(double origin, double bound); + + // @Override + public double nextExponential(); + + // @Override + public double nextGaussian(); + + // @Override + public double nextGaussian(double mean, double stddev); + +// // @Override +// public IntStream ints(long streamSize); +// +// // @Override +// public IntStream ints(); +// +// // @Override +// public IntStream ints(long streamSize, int randomNumberOrigin, int randomNumberBound); +// +// // @Override +// public IntStream ints(int randomNumberOrigin, int randomNumberBound); +// +// // @Override +// public LongStream longs(long streamSize); +// +// // @Override +// public LongStream longs(); +// +// // @Override +// public LongStream longs(long streamSize, long randomNumberOrigin, long randomNumberBound); +// +// // @Override +// public LongStream longs(long randomNumberOrigin, long randomNumberBound); +// // @Override +// public DoubleStream doubles(long streamSize); +// +// // @Override +// public DoubleStream doubles(); +// +// // @Override +// public DoubleStream doubles(long streamSize, double randomNumberOrigin, double randomNumberBound); +// // @Override +// public DoubleStream doubles(double randomNumberOrigin, double randomNumberBound); + + // @Override + public String toString(); +} \ No newline at end of file diff --git a/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/util/random/RandomGenerator.java b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/util/random/RandomGenerator.java new file mode 100644 index 00000000000..46415d0a0d9 --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/java/util/random/RandomGenerator.java @@ -0,0 +1,80 @@ +package java.util.random; + +public interface RandomGenerator { + +// public static RandomGenerator of(String name); +// +// public static RandomGenerator getDefault(); + + public void setSeed(long seed); + + public boolean isDeprecated(); + + public void nextBytes(byte[] bytes); + + public int nextInt(); + + public int nextInt(int bound); + + public int nextInt(int origin, int bound); + + public long nextLong(); + + public long nextLong(long bound); + + public long nextLong(long origin, long bound); + + public boolean nextBoolean(); + + public float nextFloat(); + + public float nextFloat(float bound); + + public float nextFloat(float origin, float bound); + + public double nextDouble(); + + public double nextDouble(double bound); + + public double nextDouble(double origin, double bound); + + public double nextExponential(); + + public double nextGaussian(); + + public double nextGaussian(double mean, double stddev); + +// +// public IntStream ints(long streamSize); +// +// +// public IntStream ints(); +// +// +// public IntStream ints(long streamSize, int randomNumberOrigin, int randomNumberBound); +// +// +// public IntStream ints(int randomNumberOrigin, int randomNumberBound); +// +// +// public LongStream longs(long streamSize); +// +// +// public LongStream longs(); +// +// +// public LongStream longs(long streamSize, long randomNumberOrigin, long randomNumberBound); +// +// +// public LongStream longs(long randomNumberOrigin, long randomNumberBound); +// +// public DoubleStream doubles(long streamSize); +// +// +// public DoubleStream doubles(); +// +// +// public DoubleStream doubles(long streamSize, double randomNumberOrigin, double randomNumberBound); +// +// public DoubleStream doubles(double randomNumberOrigin, double randomNumberBound); +} \ No newline at end of file diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java index fd1d85147d9..1329320e967 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java @@ -1213,6 +1213,14 @@ public static ProofCollection automaticJavaDL() throws IOException { g.loadable("Java/Records/Use.key"); g.loadable("Java/Records/Constructor.key"); + g = c.group("StipuLa"); + g.provable("case-studies/stipula/behavior_run_bet.key"); + g.provable("case-studies/stipula/behavior_run_bike.key"); + g.provable("case-studies/stipula/behavior_run_donation.key"); + g.provable("case-studies/stipula/behavior_run_license.key"); + g.provable("case-studies/stipula/behavior_run_loanForUse.key"); + + // use for debugging purposes. // c.keep("VSTTE10"); String s = System.getenv(ENV_KEY_RAP_FUN_KEEP); diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/sequent/Sequent.java b/key.ncore.calculus/src/main/java/org/key_project/prover/sequent/Sequent.java index 1669d04b41b..c4f0c512032 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/sequent/Sequent.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/sequent/Sequent.java @@ -502,6 +502,6 @@ public int getChildCount() { @Override public @NonNull SyntaxElement getChild(int n) { // Could also make SequentFormula a SyntaxElement; no special reason for current decision. - return getFormulaByNr(n - 1).formula(); + return getFormulaByNr(n + 1).formula(); } } diff --git a/key.ui/examples/case-studies/stipula/README.txt b/key.ui/examples/case-studies/stipula/README.txt new file mode 100644 index 00000000000..53ed72e2bfd --- /dev/null +++ b/key.ui/examples/case-studies/stipula/README.txt @@ -0,0 +1,7 @@ +These are the input files for the StipuLa case study + +Journal Article (currently under review) + +The Java files are translations from StipuLa contracts to Java files. + + diff --git a/key.ui/examples/case-studies/stipula/behavior_run_bet.key b/key.ui/examples/case-studies/stipula/behavior_run_bet.key new file mode 100644 index 00000000000..a77ea610468 --- /dev/null +++ b/key.ui/examples/case-studies/stipula/behavior_run_bet.key @@ -0,0 +1,84 @@ +\profile "Java Profile"; + +\settings { + "Choice" : { + "JavaCard" : "JavaCard:off", + "Strings" : "Strings:on", + "assertions" : "assertions:safe", + "bigint" : "bigint:on", + "finalFields" : "finalFields:immutable", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:noRestriction", + "modelFields" : "modelFields:treatAsAxiom", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "soundDefaultContracts" : "soundDefaultContracts:on" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "Modular JavaDL Strategy", + "MaximumNumberOfAutomaticApplications" : 500000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_OFF", + "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL", + "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_OFF", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_RESTRICTED", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_NORMAL", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } +} + + +\javaSource "./src/"; + +\proofObligation { + "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + "contract" : "Bet[Bet::behavior()].JML normal_behavior operation contract.0", + "name" : "Bet[Bet::behavior()].JML normal_behavior operation contract.0" +} diff --git a/key.ui/examples/case-studies/stipula/behavior_run_bike.key b/key.ui/examples/case-studies/stipula/behavior_run_bike.key new file mode 100644 index 00000000000..1e5bfae82a3 --- /dev/null +++ b/key.ui/examples/case-studies/stipula/behavior_run_bike.key @@ -0,0 +1,84 @@ +\profile "Java Profile"; + +\settings { + "Choice" : { + "JavaCard" : "JavaCard:off", + "Strings" : "Strings:on", + "assertions" : "assertions:safe", + "bigint" : "bigint:on", + "finalFields" : "finalFields:immutable", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:noRestriction", + "modelFields" : "modelFields:treatAsAxiom", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "soundDefaultContracts" : "soundDefaultContracts:on" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "Modular JavaDL Strategy", + "MaximumNumberOfAutomaticApplications" : 500000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_OFF", + "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL", + "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_OFF", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_RESTRICTED", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_NORMAL", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } +} + + +\javaSource "./src/"; + +\proofObligation { + "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + "contract" : "BikeRental[BikeRental::behavior()].JML normal_behavior operation contract.0", + "name" : "BikeRental[BikeRental::behavior()].JML normal_behavior operation contract.0" +} diff --git a/key.ui/examples/case-studies/stipula/behavior_run_donation.key b/key.ui/examples/case-studies/stipula/behavior_run_donation.key new file mode 100644 index 00000000000..99f84633b5f --- /dev/null +++ b/key.ui/examples/case-studies/stipula/behavior_run_donation.key @@ -0,0 +1,84 @@ +\profile "Java Profile"; + +\settings { + "Choice" : { + "JavaCard" : "JavaCard:off", + "Strings" : "Strings:on", + "assertions" : "assertions:safe", + "bigint" : "bigint:on", + "finalFields" : "finalFields:immutable", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:noRestriction", + "modelFields" : "modelFields:treatAsAxiom", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "soundDefaultContracts" : "soundDefaultContracts:on" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "Modular JavaDL Strategy", + "MaximumNumberOfAutomaticApplications" : 500000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_OFF", + "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL", + "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_OFF", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_RESTRICTED", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_NORMAL", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } +} + + +\javaSource "./src/"; + +\proofObligation { + "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + "contract" : "DonationMatching[DonationMatching::behavior()].JML normal_behavior operation contract.0", + "name" : "DonationMatching[DonationMatching::behavior()].JML normal_behavior operation contract.0" +} diff --git a/key.ui/examples/case-studies/stipula/behavior_run_license.key b/key.ui/examples/case-studies/stipula/behavior_run_license.key new file mode 100644 index 00000000000..2eee2cbd732 --- /dev/null +++ b/key.ui/examples/case-studies/stipula/behavior_run_license.key @@ -0,0 +1,84 @@ +\profile "Java Profile"; + +\settings { + "Choice" : { + "JavaCard" : "JavaCard:off", + "Strings" : "Strings:on", + "assertions" : "assertions:safe", + "bigint" : "bigint:on", + "finalFields" : "finalFields:immutable", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:noRestriction", + "modelFields" : "modelFields:treatAsAxiom", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "soundDefaultContracts" : "soundDefaultContracts:on" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "Modular JavaDL Strategy", + "MaximumNumberOfAutomaticApplications" : 500000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_OFF", + "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL", + "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_OFF", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_RESTRICTED", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_NORMAL", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } +} + + +\javaSource "./src/"; + +\proofObligation { + "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + "contract" : "License[License::behavior()].JML normal_behavior operation contract.0", + "name" : "License[License::behavior()].JML normal_behavior operation contract.0" +} diff --git a/key.ui/examples/case-studies/stipula/behavior_run_loanForUse.key b/key.ui/examples/case-studies/stipula/behavior_run_loanForUse.key new file mode 100644 index 00000000000..e2910ef33de --- /dev/null +++ b/key.ui/examples/case-studies/stipula/behavior_run_loanForUse.key @@ -0,0 +1,84 @@ +\profile "Java Profile"; + +\settings { + "Choice" : { + "JavaCard" : "JavaCard:off", + "Strings" : "Strings:on", + "assertions" : "assertions:safe", + "bigint" : "bigint:on", + "finalFields" : "finalFields:immutable", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:noRestriction", + "modelFields" : "modelFields:treatAsAxiom", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "soundDefaultContracts" : "soundDefaultContracts:on" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "Modular JavaDL Strategy", + "MaximumNumberOfAutomaticApplications" : 500000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE", + "DEP_OPTIONS_KEY" : "DEP_OFF", + "HEAP_REDUCTION_OPTIONS_KEY" : "HEAP_REDUCTION_NORMAL", + "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_OFF", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_RESTRICTED", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_NORMAL", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "TRIGGERS_OPTIONS_KEY" : "TRIGGERS_BEST", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } +} + + +\javaSource "./src/"; + +\proofObligation { + "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO", + "contract" : "LoanForUse[LoanForUse::behavior()].JML normal_behavior operation contract.0", + "name" : "LoanForUse[LoanForUse::behavior()].JML normal_behavior operation contract.0" +} diff --git a/key.ui/examples/case-studies/stipula/src/Bet.java b/key.ui/examples/case-studies/stipula/src/Bet.java new file mode 100644 index 00000000000..981ebd7c6af --- /dev/null +++ b/key.ui/examples/case-studies/stipula/src/Bet.java @@ -0,0 +1,515 @@ +import java.util.Random; +public class Bet { + private static Random random = new Random(); + public final static int Init = 0; + public final static int First = 1; + public final static int Fail = 2; + public final static int Run = 3; + public final static int End = 4; + //@ public invariant -1 <= currentState < 5; + public static int currentState = -1; + //@ public static invariant wallet1 >= 0; + public static int wallet1; + //@ public static invariant Better1_wallet1 >= 0; + public static int Better1_wallet1; + //@ public static invariant Better2_wallet1 >= 0; + public static int Better2_wallet1; + //@ public static invariant DataProvider_wallet1 >= 0; + public static int DataProvider_wallet1; + //@ public static invariant wallet2 >= 0; + public static int wallet2; + //@ public static invariant Better1_wallet2 >= 0; + public static int Better1_wallet2; + //@ public static invariant Better2_wallet2 >= 0; + public static int Better2_wallet2; + //@ public static invariant DataProvider_wallet2 >= 0; + public static int DataProvider_wallet2; + + public static int Better1; + public static int Better2; + public static int DataProvider; + + public static int val1; + public static int val2; + public static int event; + public static int amount; + //@ public static invariant t_before >= 0; + public static int t_before; + //@ public static invariant t_after >= 0; + public static int t_after; + //@ public static invariant now >= 0; + public static int now = 0; + //@ public static invariant DT_MIN.length == 2; + //@ public static invariant DT_MAX.length == DT_MIN.length && DT_MIN != DT_MAX; + //@ public static invariant (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] <= DT_MAX[i]); + public static int[] DT_MIN = new int[2]; + public static int[] DT_MAX = new int[2]; + + // create unique name by prefixing function name tp parameter name + public static int place_bet_x; + public static int place_bet_h; + // create unique name by prefixing function name tp parameter name + public static int place_bet2_x; + public static int place_bet2_h; + // create unique name by prefixing function name tp parameter name + public static int data_x, data_z; + //@ public static invariant ( 0 <= t_before < t_after && amount > 0 ); + /*@ model two_state static boolean assetPreservation() { + return wallet1 + Better1_wallet1 + Better2_wallet1 + DataProvider_wallet1 == \old(wallet1 + Better1_wallet1 + Better2_wallet1 + DataProvider_wallet1) && wallet2 + Better1_wallet2 + Better2_wallet2 + DataProvider_wallet2 == \old(wallet2 + Better1_wallet2 + Better2_wallet2 + DataProvider_wallet2); + } */ + // functions of the stipula contract + /*@ public normal_behavior + @ requires ((h == amount) && Better1_wallet1 >= h); + @ requires h >= 0 && Better1_wallet1 >= h; + @ assignable wallet1, val1, Better1_wallet1, DT_MIN[0], DT_MAX[0]; + @ ensures wallet1 == \old(wallet1 + h) && val1 == x && Better1_wallet1 == \old(Better1_wallet1 - h); + @ ensures ( \old(DT_MIN[0] == -1 && DT_MAX[0] == -1) ? + @ DT_MIN[0] == now + t_before && DT_MAX[0] == now + t_before + @ : ( + @ ( DT_MAX[0] == (now + t_before > \old(DT_MAX[0]) ? + @ now + t_before : \old(DT_MAX[0]))) + @ && DT_MIN[0] == \old(DT_MIN[0]) + @ ) + @ ); + @ ensures assetPreservation(); + @*/ + public static void place_bet(int x, int h) { + int tmp_0 = h; Better1_wallet1 = Better1_wallet1 - tmp_0;wallet1 = wallet1 + tmp_0; // asset transfer + val1 = x; + int new_time; + new_time = now + t_before; + if (DT_MIN[0] == -1 && DT_MAX[0] == -1) { + DT_MIN[0] = new_time; + DT_MAX[0] = new_time; + } else if (DT_MAX[0] < new_time) { + DT_MAX[0] = new_time; + } + } + /*@ public normal_behavior + @ requires ((h == amount) && Better2_wallet2 >= h); + @ requires h >= 0 && Better2_wallet2 >= h; + @ assignable wallet2, val2, Better2_wallet2, DT_MIN[1], DT_MAX[1]; + @ ensures wallet2 == \old(wallet2 + h) && val2 == x && Better2_wallet2 == \old(Better2_wallet2 - h); + @ ensures ( \old(DT_MIN[1] == -1 && DT_MAX[1] == -1) ? + @ DT_MIN[1] == now + t_after && DT_MAX[1] == now + t_after + @ : ( + @ ( DT_MAX[1] == (now + t_after > \old(DT_MAX[1]) ? + @ now + t_after : \old(DT_MAX[1]))) + @ && DT_MIN[1] == \old(DT_MIN[1]) + @ ) + @ ); + @ ensures assetPreservation(); + @*/ + public static void place_bet2(int x, int h) { + int tmp_1 = h; Better2_wallet2 = Better2_wallet2 - tmp_1;wallet2 = wallet2 + tmp_1; // asset transfer + val2 = x; + int new_time; + new_time = now + t_after; + if (DT_MIN[1] == -1 && DT_MAX[1] == -1) { + DT_MIN[1] = new_time; + DT_MAX[1] = new_time; + } else if (DT_MAX[1] < new_time) { + DT_MAX[1] = new_time; + } + } + /*@ public normal_behavior + @ requires ((x == event)); + @ assignable wallet2, wallet1, Better1_wallet2, Better1_wallet1, Better2_wallet1, DataProvider_wallet1, DataProvider_wallet2, Better2_wallet2; + @ ensures wallet2 == \old(((z == val1) && (z == val2)) ? 0 : (((z == val1) && (z != val2)) ? 0 : (((z != val1) && (z == val2)) ? 0 : 0))) && wallet1 == \old(((z == val1) && (z == val2)) ? 0 : (((z == val1) && (z != val2)) ? 0 : (((z != val1) && (z == val2)) ? 0 : 0))) && Better1_wallet2 == \old(((z == val1) && (z == val2)) ? Better1_wallet2 : (((z == val1) && (z != val2)) ? (Better1_wallet2 + wallet2) : Better1_wallet2)) && Better1_wallet1 == \old(((z == val1) && (z == val2)) ? (Better1_wallet1 + wallet1) : (((z == val1) && (z != val2)) ? (Better1_wallet1 + wallet1) : Better1_wallet1)) && Better2_wallet1 == \old(((z == val1) && (z == val2)) ? Better2_wallet1 : (((z == val1) && (z != val2)) ? Better2_wallet1 : (((z != val1) && (z == val2)) ? (Better2_wallet1 + wallet1) : Better2_wallet1))) && DataProvider_wallet1 == \old(((z == val1) && (z == val2)) ? DataProvider_wallet1 : (((z == val1) && (z != val2)) ? DataProvider_wallet1 : (((z != val1) && (z == val2)) ? DataProvider_wallet1 : (DataProvider_wallet1 + wallet1)))) && DataProvider_wallet2 == \old(((z == val1) && (z == val2)) ? DataProvider_wallet2 : (((z == val1) && (z != val2)) ? DataProvider_wallet2 : (((z != val1) && (z == val2)) ? DataProvider_wallet2 : (DataProvider_wallet2 + wallet2)))) && Better2_wallet2 == \old(((z == val1) && (z == val2)) ? (Better2_wallet2 + wallet2) : (((z == val1) && (z != val2)) ? Better2_wallet2 : (((z != val1) && (z == val2)) ? (Better2_wallet2 + wallet2) : Better2_wallet2))); + @ ensures assetPreservation(); + @*/ + public static void data(int x, int z) { + if (((z == val1) && (z == val2))) { + int tmp_2 = wallet1; wallet1 = wallet1 - tmp_2;Better1_wallet1 = Better1_wallet1 + tmp_2; // asset transfer +int tmp_3 = wallet2; wallet2 = wallet2 - tmp_3;Better2_wallet2 = Better2_wallet2 + tmp_3; // asset transfer + } else { + if (((z == val1) && (z != val2))) { + int tmp_4 = wallet2; wallet2 = wallet2 - tmp_4;Better1_wallet2 = Better1_wallet2 + tmp_4; // asset transfer +int tmp_5 = wallet1; wallet1 = wallet1 - tmp_5;Better1_wallet1 = Better1_wallet1 + tmp_5; // asset transfer + } else { + if (((z != val1) && (z == val2))) { + int tmp_6 = wallet1; wallet1 = wallet1 - tmp_6;Better2_wallet1 = Better2_wallet1 + tmp_6; // asset transfer +int tmp_7 = wallet2; wallet2 = wallet2 - tmp_7;Better2_wallet2 = Better2_wallet2 + tmp_7; // asset transfer + } else { + int tmp_8 = wallet2; wallet2 = wallet2 - tmp_8;DataProvider_wallet2 = DataProvider_wallet2 + tmp_8; // asset transfer +int tmp_9 = wallet1; wallet1 = wallet1 - tmp_9;DataProvider_wallet1 = DataProvider_wallet1 + tmp_9; // asset transfer + } + } + } + } + // event functions + /*@ public normal_behavior + @ requires wallet1 >= wallet1; + @ assignable wallet1, Better1_wallet1; + @ ensures wallet1 == 0 && Better1_wallet1 == \old(Better1_wallet1 + wallet1); + @ ensures wallet1 == 0 && Better1_wallet1 == \old(Better1_wallet1 + wallet1); + @ ensures assetPreservation(); + @*/ + public static void event_0() { + int tmp_10 = wallet1; wallet1 = wallet1 - tmp_10;Better1_wallet1 = Better1_wallet1 + tmp_10; // asset transfer + } + /*@ public normal_behavior + @ requires wallet1 >= wallet1 && wallet2 >= wallet2; + @ assignable wallet2, wallet1, Better1_wallet1, Better2_wallet2; + @ ensures wallet2 == 0 && wallet1 == 0 && Better1_wallet1 == \old(Better1_wallet1 + wallet1) && Better2_wallet2 == \old(Better2_wallet2 + wallet2); + @ ensures wallet2 == 0 && wallet1 == 0 && Better1_wallet1 == \old(Better1_wallet1 + wallet1) && Better2_wallet2 == \old(Better2_wallet2 + wallet2); + @ ensures assetPreservation(); + @*/ + public static void event_1() { + int tmp_11 = wallet1; wallet1 = wallet1 - tmp_11;Better1_wallet1 = Better1_wallet1 + tmp_11; // asset transfer + int tmp_12 = wallet2; wallet2 = wallet2 - tmp_12;Better2_wallet2 = Better2_wallet2 + tmp_12; // asset transfer + } + // behavior + /*@ public normal_behavior + @ requires ( wallet1 == 0 && wallet2 == 0 ); + @ ensures ( assetPreservation() ) && ( currentState == Fail ==> (wallet1 == 0 && wallet2 == 0 && Better1_wallet1==\old(Better1_wallet1) && Better1_wallet2==\old(Better1_wallet2) && Better2_wallet1==\old(Better2_wallet1) && Better2_wallet2==\old(Better2_wallet2)) ); + @ assignable \everything; + @*/ + public static void behavior() { + currentState = -1; + resetDispatch(); + GenInit(); + } + + // GEN_C(Q) for state that does not occur on a cycle + public static void GenInit() { + currentState = Init; + int next_action = computeNextStepEmptyEvents(1); + //@ assume next_action < 0 || (next_action > 0 ? Init_evalConditionFor(next_action) : false); + switch (next_action) { + case 1: + place_bet(place_bet_x, place_bet_h); + GenFirst(); + break; + default: break; + } + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenFirst() { + currentState = First; + int next_action = computeNextStep(1, new int[] { 0 }); + //@ assume next_action < 0 || (next_action > 0 ? First_evalConditionFor(next_action) : false); + switch (next_action) { + case 1: + place_bet2(place_bet2_x, place_bet2_h); + GenRun(); + break; + case -1: + event_0(); + DT_MIN[0] = -1; + DT_MAX[0] = -1; + GenFail(); + break; + default: break; + } + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenFail() { + currentState = Fail; + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenRun() { + currentState = Run; + int next_action = computeNextStep(1, new int[] { 1 }); + //@ assume next_action < 0 || (next_action > 0 ? Run_evalConditionFor(next_action) : false); + switch (next_action) { + case 1: + data(data_x, data_z); + GenEnd(); + break; + case -2: + event_1(); + DT_MIN[1] = -1; + DT_MAX[1] = -1; + GenFail(); + break; + default: break; + } + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenEnd() { + currentState = End; + } + + + + // auxiliary methods + public final static int computeNextStepNoFunctions(int[] events){ + int entry = minTimeEntry(events); + if (entry == -1) { + return -(events.length + 1); + } else if (DT_MIN[entry] >= now) { + now = DT_MIN[entry]; + } + return -(entry + 1); + } + public final static int computeNextStepEmptyEvents(int nrFct){ + if (nrFct == 0) { + return -1; + } else { + int max_entry = maxTimeEntry(); + int max_time = max_entry == -1 ? now : DT_MAX[max_entry] + 1; + int u_Q = choose(now, max_time); + now = u_Q; + return choose(1,nrFct); + } + } + public final static int computeNextStep(int nrFct, int[] events){ + int w_Q; + int entry = minTimeEntry(events); + int max_entry = maxTimeEntry(); + int max_time = (max_entry == -1 ? now : DT_MAX[max_entry] + 1); + int u_Q = choose(now, max_time); + if (entry == -1) { + w_Q = choose(1,nrFct); + now = u_Q; + return w_Q; + } else { + int dtMaxEntry = DT_MAX[entry]; + int dtMinEntry = DT_MIN[entry]; + if ((dtMinEntry == now) ? true : (dtMaxEntry == now)) { + return -(entry + 1); + } else { + w_Q = choose(0, nrFct); + if (w_Q != 0) { + int timeval = maxSafeTimeIncrement(events); + now = (dtMinEntry < now ? min(dtMinEntry - 1, u_Q) : min(max(timeval-1, now), u_Q)); + return w_Q; + } else { + now = (dtMinEntry < now ? now : dtMinEntry); + return -(entry + 1); + } + } + } + } + /*@ public normal_behavior + @ requires DT_MIN != null && DT_MAX != null & DT_MIN.length == DT_MAX.length; + @ requires events.length <= DT_MIN.length; + @ requires (\forall int i; 0 <= i < events.length; 0 <= events[i] < DT_MIN.length); + @ requires (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] <= DT_MAX[i]); + @ requires now >= 0; + @ ensures \result == -1 || \result >= now; + @ ensures \result == -1 <==> (\forall int i; 0 <= i < events.length; DT_MAX[events[i]] < now ); + @ ensures \result >= now ==> + @ (\exists int i; 0 <= i < events.length; \result == DT_MIN[events[i]] || \result == DT_MAX[events[i]]) + @ && (\forall int i; 0 <= i < events.length; + @ (DT_MIN[events[i]] >= now ==> \result <= DT_MIN[events[i]]) + @ && (DT_MIN[events[i]] < now && DT_MAX[events[i]] >= now ==> \result <= DT_MAX[events[i]])); + @ assignable \strictly_nothing; + @ + @*/ + public /*@ helper @*/ static int maxSafeTimeIncrement(int[] events) { + int res = -1; + /*@ loop_invariant 0 <= j <= events.length; + @ loop_invariant res == -1 || res >= now; + @ loop_invariant res == -1 <==> (\forall int i; 0 <= i < j; DT_MAX[events[i]] < now ); + @ loop_invariant res >= now ==> + @ (\exists int i; 0 <= i < j; (res == DT_MIN[events[i]]) || (res == DT_MAX[events[i]])) + @ && (\forall int i; 0 <= i < j; + @ (DT_MIN[events[i]] >= now ==> res <= DT_MIN[events[i]]) + @ && (DT_MIN[events[i]] < now && DT_MAX[events[i]] >= now ==> res <= DT_MAX[events[i]])); + @ assignable \strictly_nothing; + @ decreases events.length - j; + @*/ + for (int j = 0; j < events.length; j++) { + final int event = events[j]; + if (res == -1 && DT_MAX[event] >= now) { + res = DT_MAX[event]; + } + if (DT_MIN[event] >= now && res > DT_MIN[event]) { + res = DT_MIN[event]; + } else if (DT_MIN[event] < now && DT_MAX[event] >= now && res > DT_MAX[event]) { + res = DT_MAX[event]; + } + } + return res; + } + // while proving we only use the contract and hence have a non-deterministic choice + // executing the implementation chooses a value randomly + /*@ public normal_behavior + @ requires random != null; + @ requires -1 <= lower <= upper; + @ ensures lower <= \result <= upper; + @ assignable \nothing; + */ + private /*@ helper @*/ static int choose(int lower, int upper) { + return random.nextInt(upper + 1 - lower) + lower; + } + /** + * Note: note implementation is deterministic, non-deterministic behavior by underspecification + * in contract only + */ + /*@ public normal_behavior + @ requires DT_MIN != null && DT_MAX != null & DT_MIN.length == DT_MAX.length; + @ requires events.length <= DT_MIN.length; + @ requires (\forall int i; 0 <= i < events.length; 0 <= events[i] < DT_MIN.length); + @ requires (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] <= DT_MAX[i]); + @ ensures -1 <= \result < DT_MIN.length; + @ ensures \result == -1 <==> (\forall int i; 0 <= i < events.length; DT_MAX[events[i]] < now); + @ ensures \result != -1 ==> + @ ( DT_MAX[\result] >= now + @ && (\forall int j; 0 <= j < events.length; + @ ((DT_MIN[events[j]] < now && DT_MAX[events[j]] >= now) ==> DT_MIN[\result] <= DT_MAX[events[j]]) + @ && (DT_MIN[events[j]] >= now ==> DT_MIN[\result] <= DT_MIN[events[j]]) + @ ) + @ && (\exists int j; 0 <= j < events.length; \result == events[j]) + @ ); + @ assignable \strictly_nothing; + @*/ + public static /*@ helper @*/ int minTimeEntry(int[] events) { + if (events.length == 0) { + return -1; + } + int minEvent = -1; + /*@ loop_invariant + @ 0 <= i <= events.length + @ && -1 <= minEvent < DT_MIN.length + @ && (minEvent == -1 ? (\forall int j; 0 <= j < i; DT_MAX[events[j]] < now) : + @ ( DT_MAX[minEvent] >= now + @ && (\forall int j; 0 <= j < i; + @ ((DT_MIN[events[j]] < now && DT_MAX[events[j]] >= now) ==> DT_MIN[minEvent] <= DT_MAX[events[j]]) + @ && (DT_MIN[events[j]] >= now ==> DT_MIN[minEvent] <= DT_MIN[events[j]]) + @ ) + @ && (\exists int j; 0 <= j < i; minEvent == events[j]) ) + @ ); + @ assignable \strictly_nothing; + @ decreases events.length - i; + */ + for (int i = 0; i < events.length; i++) { + if (DT_MAX[events[i]] >= now) { + if (minEvent == -1) { + minEvent = events[i]; + } else if (DT_MIN[events[i]] < now && DT_MAX[events[i]] >= now && DT_MAX[events[i]] < DT_MIN[minEvent]) { + minEvent = events[i]; + } else if (DT_MIN[events[i]] >= now && DT_MIN[minEvent] > DT_MIN[events[i]]) { + minEvent = events[i]; + } + } + } + return minEvent; + } + /** + * Note: note implementation is deterministic, non-deterministic behavior by underspecification + * in contract only + */ + /*@ public normal_behavior + @ requires DT_MAX != null; + @ ensures -1 <= \result < DT_MAX.length; + @ ensures \result != -1 ==> (DT_MAX.length > 0 && DT_MAX[\result] >= now && + @ (\forall int j; 0 <= j < DT_MAX.length; DT_MAX[j] <= DT_MAX[\result])); + @ ensures \result == -1 <==> (\forall int j; 0 <= j < DT_MAX.length; DT_MAX[j] < now); + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int maxTimeEntry() { + if (DT_MAX.length == 0) { + return -1; + } + int maxEntry = -1; + /*@ loop_invariant + @ i >= 0 && i <= DT_MAX.length && + @ -1 <= maxEntry < DT_MAX.length && + @ (maxEntry != -1 ==> (DT_MAX[maxEntry] >= now && ( \forall int j; 0 <= j < i; DT_MAX[maxEntry] >= DT_MAX[j]))) && + @ (maxEntry == -1 <==> ( \forall int j; 0 <= j < i; DT_MAX[j] < now)); + @ assignable \strictly_nothing; + @ decreases DT_MAX.length - i; + */ + for (int i = 0; i < DT_MAX.length; i++) { + if (DT_MAX[i] >= now && (maxEntry == -1 || DT_MAX[i] > DT_MAX[maxEntry])) { + maxEntry = i; + } + } + return maxEntry; + } + /*@ private normal_behavior + @ requires DT_MIN != null && DT_MAX != null && DT_MIN.length == DT_MAX.length; + @ ensures (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] == -1); + @ ensures (\forall int i; 0 <= i < DT_MAX.length; DT_MAX[i] == -1); + @ assignable DT_MIN[*], DT_MAX[*]; + @*/ + private static /*@ helper @*/ void resetDispatch() { + /*@ loop_invariant + @ 0 <= i <= DT_MIN.length + @ && (\forall int j; 0 <= j < i; DT_MIN[j] == -1) + @ && (\forall int j; 0 <= j < i; DT_MAX[j] == -1); + @ assignable DT_MIN[*], DT_MAX[*]; + @ decreases DT_MIN.length - i; + @*/ + for (int i = 0; i < DT_MIN.length; i++) { + DT_MIN[i] = -1; + DT_MAX[i] = -1; + } + } + /*@ public normal_behavior + @ ensures \result == (a <= b ? a : b); + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int min(int a, int b) { + return (a <= b) ? a : b; + } + /*@ public normal_behavior + @ ensures \result == (a >= b ? a : b); + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int max(int a, int b) { + return (a >= b) ? a : b; + } + /*@ public normal_behavior + @ requires (\forall int j; 0 <= j < e.length; e[j] >= 0); + @ ensures e.length > 0 ? ((\forall int j; 0 <= j < e.length; \result >= e[j]) + @ && (\exists int j; 0 <= j < e.length; \result == e[j])) : \result == 0; + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int max(int[] e) { + int max = 0; + /*@ loop_invariant + @ i >= 0 && i <= e.length + @ && (\forall int j; 0 <= j < i; max >= e[j]) + @ && (i>0 ==> (\exists int j; 0 <= j < i; max == e[j])) + @ && (i == 0 ==> max == 0) ; + @ assignable \strictly_nothing; + @ decreases e.length - i; + */ + for (int i = 0; i < e.length; i++) { + if (max < e[i]) { + max = e[i]; + } + } + return max; + } +// evaluating function conditions + + private static boolean place_bet_cond(int x, int h) { + return ((h == amount) && Better1_wallet1 >= h); + } + + private static boolean place_bet2_cond(int x, int h) { + return ((h == amount) && Better2_wallet2 >= h); + } + + private static boolean data_cond(int x, int z) { + return ((x == event)); + } + + private static boolean Init_evalConditionFor(int fct) { + switch(fct) { + case 1: return place_bet_cond(place_bet_x, place_bet_h); + default: return false; + } + } + + private static boolean First_evalConditionFor(int fct) { + switch(fct) { + case 1: return place_bet2_cond(place_bet2_x, place_bet2_h); + default: return false; + } + } + + + private static boolean Run_evalConditionFor(int fct) { + switch(fct) { + case 1: return data_cond(data_x, data_z); + default: return false; + } + } + +} \ No newline at end of file diff --git a/key.ui/examples/case-studies/stipula/src/BikeRental.java b/key.ui/examples/case-studies/stipula/src/BikeRental.java new file mode 100644 index 00000000000..8966eac0aae --- /dev/null +++ b/key.ui/examples/case-studies/stipula/src/BikeRental.java @@ -0,0 +1,561 @@ +import java.util.Random; +public class BikeRental { + private static Random random = new Random(); + public final static int Inactive = 0; + public final static int Payment = 1; + public final static int Using = 2; + public final static int Return = 3; + public final static int EndNoDispute = 4; + public final static int Dispute = 5; + public final static int End = 6; + //@ public invariant -1 <= currentState < 7; + public static int currentState = -1; + //@ public static invariant wallet >= 0; + public static int wallet; + //@ public static invariant Lender_wallet >= 0; + public static int Lender_wallet; + //@ public static invariant Borrower_wallet >= 0; + public static int Borrower_wallet; + //@ public static invariant Authority_wallet >= 0; + public static int Authority_wallet; + + public static int Lender; + public static int Borrower; + public static int Authority; + + public static int cost; + //@ public static invariant rentingTime >= 0; + public static int rentingTime; + public static int code; + //@ public static invariant now >= 0; + public static int now = 0; + //@ public static invariant DT_MIN.length == 1; + //@ public static invariant DT_MAX.length == DT_MIN.length && DT_MIN != DT_MAX; + //@ public static invariant (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] <= DT_MAX[i]); + public static int[] DT_MIN = new int[1]; + public static int[] DT_MAX = new int[1]; + + // create unique name by prefixing function name tp parameter name + public static int offer_x; + public static int pay_h; + + // create unique name by prefixing function name tp parameter name + public static int disputeL1_x; + // create unique name by prefixing function name tp parameter name + public static int disputeL2_x; + // create unique name by prefixing function name tp parameter name + public static int disputeB1_x; + // create unique name by prefixing function name tp parameter name + public static int disputeB2_x; + // create unique name by prefixing function name tp parameter name + public static int verdict_x, verdict_y; + //@ public static invariant ( rentingTime > 0 && cost >= 0 ); + /*@ model two_state static boolean assetPreservation() { + return wallet + Lender_wallet + Borrower_wallet + Authority_wallet == \old(wallet + Lender_wallet + Borrower_wallet + Authority_wallet); + } */ + // functions of the stipula contract + /*@ public normal_behavior + @ requires (true); + @ assignable code; + @ ensures code == x; + @ ensures assetPreservation(); + @*/ + public static void offer(int x) { + code = x; + } + /*@ public normal_behavior + @ requires ((h == cost) && Borrower_wallet >= h); + @ requires h >= 0 && Borrower_wallet >= h; + @ assignable wallet, Borrower_wallet, DT_MIN[0], DT_MAX[0]; + @ ensures wallet == \old(wallet + h) && Borrower_wallet == \old(Borrower_wallet - h); + @ ensures ( \old(DT_MIN[0] == -1 && DT_MAX[0] == -1) ? + @ DT_MIN[0] == now + rentingTime && DT_MAX[0] == now + rentingTime + @ : ( + @ ( DT_MAX[0] == (now + rentingTime > \old(DT_MAX[0]) ? + @ now + rentingTime : \old(DT_MAX[0]))) + @ && DT_MIN[0] == \old(DT_MIN[0]) + @ ) + @ ); + @ ensures assetPreservation(); + @*/ + public static void pay(int h) { + int tmp_0 = h; Borrower_wallet = Borrower_wallet - tmp_0;wallet = wallet + tmp_0; // asset transfer + + int new_time; + new_time = now + rentingTime; + if (DT_MIN[0] == -1 && DT_MAX[0] == -1) { + DT_MIN[0] = new_time; + DT_MAX[0] = new_time; + } else if (DT_MAX[0] < new_time) { + DT_MAX[0] = new_time; + } + } + /*@ public normal_behavior + @ requires (true); + @ assignable \nothing; + @ ensures true; + @ ensures assetPreservation(); + @*/ + public static void end() { + + } + /*@ public normal_behavior + @ requires (true); + @ requires wallet >= wallet; + @ assignable wallet, Lender_wallet; + @ ensures wallet == 0 && Lender_wallet == \old(Lender_wallet + wallet); + @ ensures assetPreservation(); + @*/ + public static void rentalOk() { + int tmp_1 = wallet; wallet = wallet - tmp_1;Lender_wallet = Lender_wallet + tmp_1; // asset transfer + } + /*@ public normal_behavior + @ requires (true); + @ assignable \nothing; + @ ensures true; + @ ensures assetPreservation(); + @*/ + public static void disputeL1(int x) { + + } + /*@ public normal_behavior + @ requires (true); + @ assignable \nothing; + @ ensures true; + @ ensures assetPreservation(); + @*/ + public static void disputeL2(int x) { + + } + /*@ public normal_behavior + @ requires (true); + @ assignable \nothing; + @ ensures true; + @ ensures assetPreservation(); + @*/ + public static void disputeB1(int x) { + + } + /*@ public normal_behavior + @ requires (true); + @ assignable \nothing; + @ ensures true; + @ ensures assetPreservation(); + @*/ + public static void disputeB2(int x) { + + } + /*@ public normal_behavior + @ requires (((y >= 0) && (y <= 1))); + @ requires wallet >= (y * wallet) && wallet >= wallet; + @ assignable wallet, Lender_wallet, Borrower_wallet; + @ ensures wallet == 0 && Lender_wallet == \old(Lender_wallet + (y * wallet)) && Borrower_wallet == \old(Borrower_wallet + (wallet - (y * wallet))); + @ ensures assetPreservation(); + @*/ + public static void verdict(int x, int y) { + + + int tmp_2 = (y * wallet); wallet = wallet - tmp_2;Lender_wallet = Lender_wallet + tmp_2; // asset transfer + int tmp_3 = wallet; wallet = wallet - tmp_3;Borrower_wallet = Borrower_wallet + tmp_3; // asset transfer + } + // event functions + /*@ public normal_behavior + @ assignable \nothing; + @ ensures true; + @ ensures true; + @ ensures assetPreservation(); + @*/ + public static void event_0() { + + } + // behavior + /*@ public normal_behavior + @ requires ( Borrower_wallet >= cost && wallet == 0 ); + @ ensures ( currentState == EndNoDispute ==> (wallet == 0 && Lender_wallet == \old(Lender_wallet) + (\old(Borrower_wallet) - Borrower_wallet)) ); + @ assignable \everything; + @*/ + public static void behavior() { + currentState = -1; + resetDispatch(); + GenInactive(); + } + + // GEN_C(Q) for state that does not occur on a cycle + public static void GenInactive() { + currentState = Inactive; + int next_action = computeNextStepEmptyEvents(1); + switch (next_action) { + case 1: + offer(offer_x); + GenPayment(); + break; + default: break; + } + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenPayment() { + currentState = Payment; + int next_action = computeNextStepEmptyEvents(1); + //@ assume next_action < 0 || (next_action > 0 ? Payment_evalConditionFor(next_action) : false); + switch (next_action) { + case 1: + pay(pay_h); + GenUsing(); + break; + default: break; + } + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenUsing() { + currentState = Using; + int next_action = computeNextStep(3, new int[] { 0 }); + switch (next_action) { + case 1: + end(); + GenReturn(); + break; + case 2: + disputeL1(disputeL1_x); + GenDispute(); + break; + case 3: + disputeB1(disputeB1_x); + GenDispute(); + break; + case -1: + event_0(); + DT_MIN[0] = -1; + DT_MAX[0] = -1; + GenReturn(); + break; + default: break; + } + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenReturn() { + currentState = Return; + int next_action = computeNextStepEmptyEvents(3); + switch (next_action) { + case 1: + rentalOk(); + GenEndNoDispute(); + break; + case 2: + disputeL2(disputeL2_x); + GenDispute(); + break; + case 3: + disputeB2(disputeB2_x); + GenDispute(); + break; + default: break; + } + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenEndNoDispute() { + currentState = EndNoDispute; + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenDispute() { + currentState = Dispute; + int next_action = computeNextStepEmptyEvents(1); + //@ assume next_action < 0 || (next_action > 0 ? Dispute_evalConditionFor(next_action) : false); + switch (next_action) { + case 1: + verdict(verdict_x, verdict_y); + GenEnd(); + break; + default: break; + } + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenEnd() { + currentState = End; + } + + + + // auxiliary methods + public final static int computeNextStepNoFunctions(int[] events){ + int entry = minTimeEntry(events); + if (entry == -1) { + return -(events.length + 1); + } else if (DT_MIN[entry] >= now) { + now = DT_MIN[entry]; + } + return -(entry + 1); + } + public final static int computeNextStepEmptyEvents(int nrFct){ + if (nrFct == 0) { + return -1; + } else { + int max_entry = maxTimeEntry(); + int max_time = max_entry == -1 ? now : DT_MAX[max_entry] + 1; + int u_Q = choose(now, max_time); + now = u_Q; + return choose(1,nrFct); + } + } + public final static int computeNextStep(int nrFct, int[] events){ + int w_Q; + int entry = minTimeEntry(events); + int max_entry = maxTimeEntry(); + int max_time = (max_entry == -1 ? now : DT_MAX[max_entry] + 1); + int u_Q = choose(now, max_time); + if (entry == -1) { + w_Q = choose(1,nrFct); + now = u_Q; + return w_Q; + } else { + int dtMaxEntry = DT_MAX[entry]; + int dtMinEntry = DT_MIN[entry]; + if ((dtMinEntry == now) ? true : (dtMaxEntry == now)) { + return -(entry + 1); + } else { + w_Q = choose(0, nrFct); + if (w_Q != 0) { + int timeval = maxSafeTimeIncrement(events); + now = (dtMinEntry < now ? min(dtMinEntry - 1, u_Q) : min(max(timeval-1, now), u_Q)); + return w_Q; + } else { + now = (dtMinEntry < now ? now : dtMinEntry); + return -(entry + 1); + } + } + } + } + /*@ public normal_behavior + @ requires DT_MIN != null && DT_MAX != null & DT_MIN.length == DT_MAX.length; + @ requires events.length <= DT_MIN.length; + @ requires (\forall int i; 0 <= i < events.length; 0 <= events[i] < DT_MIN.length); + @ requires (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] <= DT_MAX[i]); + @ requires now >= 0; + @ ensures \result == -1 || \result >= now; + @ ensures \result == -1 <==> (\forall int i; 0 <= i < events.length; DT_MAX[events[i]] < now ); + @ ensures \result >= now ==> + @ (\exists int i; 0 <= i < events.length; \result == DT_MIN[events[i]] || \result == DT_MAX[events[i]]) + @ && (\forall int i; 0 <= i < events.length; + @ (DT_MIN[events[i]] >= now ==> \result <= DT_MIN[events[i]]) + @ && (DT_MIN[events[i]] < now && DT_MAX[events[i]] >= now ==> \result <= DT_MAX[events[i]])); + @ assignable \strictly_nothing; + @ + @*/ + public /*@ helper @*/ static int maxSafeTimeIncrement(int[] events) { + int res = -1; + /*@ loop_invariant 0 <= j <= events.length; + @ loop_invariant res == -1 || res >= now; + @ loop_invariant res == -1 <==> (\forall int i; 0 <= i < j; DT_MAX[events[i]] < now ); + @ loop_invariant res >= now ==> + @ (\exists int i; 0 <= i < j; (res == DT_MIN[events[i]]) || (res == DT_MAX[events[i]])) + @ && (\forall int i; 0 <= i < j; + @ (DT_MIN[events[i]] >= now ==> res <= DT_MIN[events[i]]) + @ && (DT_MIN[events[i]] < now && DT_MAX[events[i]] >= now ==> res <= DT_MAX[events[i]])); + @ assignable \strictly_nothing; + @ decreases events.length - j; + @*/ + for (int j = 0; j < events.length; j++) { + final int event = events[j]; + if (res == -1 && DT_MAX[event] >= now) { + res = DT_MAX[event]; + } + if (DT_MIN[event] >= now && res > DT_MIN[event]) { + res = DT_MIN[event]; + } else if (DT_MIN[event] < now && DT_MAX[event] >= now && res > DT_MAX[event]) { + res = DT_MAX[event]; + } + } + return res; + } + // while proving we only use the contract and hence have a non-deterministic choice + // executing the implementation chooses a value randomly + /*@ public normal_behavior + @ requires random != null; + @ requires -1 <= lower <= upper; + @ ensures lower <= \result <= upper; + @ assignable \nothing; + */ + private /*@ helper @*/ static int choose(int lower, int upper) { + return random.nextInt(upper + 1 - lower) + lower; + } + /** + * Note: note implementation is deterministic, non-deterministic behavior by underspecification + * in contract only + */ + /*@ public normal_behavior + @ requires DT_MIN != null && DT_MAX != null & DT_MIN.length == DT_MAX.length; + @ requires events.length <= DT_MIN.length; + @ requires (\forall int i; 0 <= i < events.length; 0 <= events[i] < DT_MIN.length); + @ requires (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] <= DT_MAX[i]); + @ ensures -1 <= \result < DT_MIN.length; + @ ensures \result == -1 <==> (\forall int i; 0 <= i < events.length; DT_MAX[events[i]] < now); + @ ensures \result != -1 ==> + @ ( DT_MAX[\result] >= now + @ && (\forall int j; 0 <= j < events.length; + @ ((DT_MIN[events[j]] < now && DT_MAX[events[j]] >= now) ==> DT_MIN[\result] <= DT_MAX[events[j]]) + @ && (DT_MIN[events[j]] >= now ==> DT_MIN[\result] <= DT_MIN[events[j]]) + @ ) + @ && (\exists int j; 0 <= j < events.length; \result == events[j]) + @ ); + @ assignable \strictly_nothing; + @*/ + public static /*@ helper @*/ int minTimeEntry(int[] events) { + if (events.length == 0) { + return -1; + } + int minEvent = -1; + /*@ loop_invariant + @ 0 <= i <= events.length + @ && -1 <= minEvent < DT_MIN.length + @ && (minEvent == -1 ? (\forall int j; 0 <= j < i; DT_MAX[events[j]] < now) : + @ ( DT_MAX[minEvent] >= now + @ && (\forall int j; 0 <= j < i; + @ ((DT_MIN[events[j]] < now && DT_MAX[events[j]] >= now) ==> DT_MIN[minEvent] <= DT_MAX[events[j]]) + @ && (DT_MIN[events[j]] >= now ==> DT_MIN[minEvent] <= DT_MIN[events[j]]) + @ ) + @ && (\exists int j; 0 <= j < i; minEvent == events[j]) ) + @ ); + @ assignable \strictly_nothing; + @ decreases events.length - i; + */ + for (int i = 0; i < events.length; i++) { + if (DT_MAX[events[i]] >= now) { + if (minEvent == -1) { + minEvent = events[i]; + } else if (DT_MIN[events[i]] < now && DT_MAX[events[i]] >= now && DT_MAX[events[i]] < DT_MIN[minEvent]) { + minEvent = events[i]; + } else if (DT_MIN[events[i]] >= now && DT_MIN[minEvent] > DT_MIN[events[i]]) { + minEvent = events[i]; + } + } + } + return minEvent; + } + /** + * Note: note implementation is deterministic, non-deterministic behavior by underspecification + * in contract only + */ + /*@ public normal_behavior + @ requires DT_MAX != null; + @ ensures -1 <= \result < DT_MAX.length; + @ ensures \result != -1 ==> (DT_MAX.length > 0 && DT_MAX[\result] >= now && + @ (\forall int j; 0 <= j < DT_MAX.length; DT_MAX[j] <= DT_MAX[\result])); + @ ensures \result == -1 <==> (\forall int j; 0 <= j < DT_MAX.length; DT_MAX[j] < now); + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int maxTimeEntry() { + if (DT_MAX.length == 0) { + return -1; + } + int maxEntry = -1; + /*@ loop_invariant + @ i >= 0 && i <= DT_MAX.length && + @ -1 <= maxEntry < DT_MAX.length && + @ (maxEntry != -1 ==> (DT_MAX[maxEntry] >= now && ( \forall int j; 0 <= j < i; DT_MAX[maxEntry] >= DT_MAX[j]))) && + @ (maxEntry == -1 <==> ( \forall int j; 0 <= j < i; DT_MAX[j] < now)); + @ assignable \strictly_nothing; + @ decreases DT_MAX.length - i; + */ + for (int i = 0; i < DT_MAX.length; i++) { + if (DT_MAX[i] >= now && (maxEntry == -1 || DT_MAX[i] > DT_MAX[maxEntry])) { + maxEntry = i; + } + } + return maxEntry; + } + /*@ private normal_behavior + @ requires DT_MIN != null && DT_MAX != null && DT_MIN.length == DT_MAX.length; + @ ensures (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] == -1); + @ ensures (\forall int i; 0 <= i < DT_MAX.length; DT_MAX[i] == -1); + @ assignable DT_MIN[*], DT_MAX[*]; + @*/ + private static /*@ helper @*/ void resetDispatch() { + /*@ loop_invariant + @ 0 <= i <= DT_MIN.length + @ && (\forall int j; 0 <= j < i; DT_MIN[j] == -1) + @ && (\forall int j; 0 <= j < i; DT_MAX[j] == -1); + @ assignable DT_MIN[*], DT_MAX[*]; + @ decreases DT_MIN.length - i; + @*/ + for (int i = 0; i < DT_MIN.length; i++) { + DT_MIN[i] = -1; + DT_MAX[i] = -1; + } + } + /*@ public normal_behavior + @ ensures \result == (a <= b ? a : b); + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int min(int a, int b) { + return (a <= b) ? a : b; + } + /*@ public normal_behavior + @ ensures \result == (a >= b ? a : b); + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int max(int a, int b) { + return (a >= b) ? a : b; + } + /*@ public normal_behavior + @ requires (\forall int j; 0 <= j < e.length; e[j] >= 0); + @ ensures e.length > 0 ? ((\forall int j; 0 <= j < e.length; \result >= e[j]) + @ && (\exists int j; 0 <= j < e.length; \result == e[j])) : \result == 0; + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int max(int[] e) { + int max = 0; + /*@ loop_invariant + @ i >= 0 && i <= e.length + @ && (\forall int j; 0 <= j < i; max >= e[j]) + @ && (i>0 ==> (\exists int j; 0 <= j < i; max == e[j])) + @ && (i == 0 ==> max == 0) ; + @ assignable \strictly_nothing; + @ decreases e.length - i; + */ + for (int i = 0; i < e.length; i++) { + if (max < e[i]) { + max = e[i]; + } + } + return max; + } +// evaluating function conditions + + private static boolean pay_cond(int h) { + return ((h == cost) && Borrower_wallet >= h); + } + + + + + private static boolean verdict_cond(int x, int y) { + return (((y >= 0) && (y <= 1))); + } + + private static boolean Inactive_evalConditionFor(int fct) { + return true; + } + + private static boolean Payment_evalConditionFor(int fct) { + switch(fct) { + case 1: return pay_cond(pay_h); + default: return false; + } + } + + private static boolean Using_evalConditionFor(int fct) { + return true; + } + + private static boolean Return_evalConditionFor(int fct) { + return true; + } + + + private static boolean Dispute_evalConditionFor(int fct) { + switch(fct) { + case 1: return verdict_cond(verdict_x, verdict_y); + default: return false; + } + } + +} \ No newline at end of file diff --git a/key.ui/examples/case-studies/stipula/src/DonationMatching.java b/key.ui/examples/case-studies/stipula/src/DonationMatching.java new file mode 100644 index 00000000000..bfdd27945d6 --- /dev/null +++ b/key.ui/examples/case-studies/stipula/src/DonationMatching.java @@ -0,0 +1,433 @@ +import java.util.Random; +public class DonationMatching { + private static Random random = new Random(); + public final static int Start = 0; + public final static int Collect = 1; + public final static int End = 2; + //@ public invariant -1 <= currentState < 3; + public static int currentState = -1; + //@ public static invariant wallet >= 0; + public static int wallet; + //@ public static invariant Company_wallet >= 0; + public static int Company_wallet; + //@ public static invariant Employee_wallet >= 0; + public static int Employee_wallet; + + public static int Company; + public static int Employee; + + //@ public static invariant endTime >= 0; + public static int endTime; + public static int amount; + public static int matchAmount; + public static int donationSize; + //@ public static invariant now >= 0; + public static int now = 0; + //@ public static invariant DT_MIN.length == 1; + //@ public static invariant DT_MAX.length == DT_MIN.length && DT_MIN != DT_MAX; + //@ public static invariant (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] <= DT_MAX[i]); + public static int[] DT_MIN = new int[1]; + public static int[] DT_MAX = new int[1]; + public static final int MAX_ITE_Collect = 20; + + public static int start_w; + public static int donate_w; + //@ public static invariant ( endTime == 10 && amount == 100 && matchAmount == 200 && donationSize == 10 ); + /*@ model two_state static boolean assetPreservation() { + return wallet + Company_wallet + Employee_wallet == \old(wallet + Company_wallet + Employee_wallet); + } */ + // functions of the stipula contract + /*@ public normal_behavior + @ requires ((w == matchAmount) && Company_wallet >= w); + @ requires w >= 0 && Company_wallet >= w; + @ assignable wallet, Company_wallet, DT_MIN[0], DT_MAX[0]; + @ ensures wallet == \old(wallet + w) && Company_wallet == \old(Company_wallet - w); + @ ensures ( \old(DT_MIN[0] == -1 && DT_MAX[0] == -1) ? + @ DT_MIN[0] == now + endTime && DT_MAX[0] == now + endTime + @ : ( + @ ( DT_MAX[0] == (now + endTime > \old(DT_MAX[0]) ? + @ now + endTime : \old(DT_MAX[0]))) + @ && DT_MIN[0] == \old(DT_MIN[0]) + @ ) + @ ); + @ ensures assetPreservation(); + @*/ + public static void start(int w) { + int tmp_0 = w; Company_wallet = Company_wallet - tmp_0;wallet = wallet + tmp_0; // asset transfer + int new_time; + new_time = now + endTime; + if (DT_MIN[0] == -1 && DT_MAX[0] == -1) { + DT_MIN[0] = new_time; + DT_MAX[0] = new_time; + } else if (DT_MAX[0] < new_time) { + DT_MAX[0] = new_time; + } + } + /*@ public normal_behavior + @ requires (true && Employee_wallet >= w); + @ requires w >= 0 && Employee_wallet >= w; + @ assignable Employee_wallet, wallet; + @ ensures Employee_wallet == \old(Employee_wallet - w) && wallet == \old(wallet + w); + @ ensures assetPreservation(); + @*/ + public static void donate(int w) { + int tmp_1 = w; Employee_wallet = Employee_wallet - tmp_1;wallet = wallet + tmp_1; // asset transfer + } + // event functions + /*@ public normal_behavior + @ assignable Company_wallet, wallet; + @ ensures Company_wallet == \old(((wallet >= matchAmount) && (wallet < (matchAmount + amount))) ? (Company_wallet + matchAmount) : Company_wallet) && wallet == \old(((wallet >= matchAmount) && (wallet < (matchAmount + amount))) ? (wallet - matchAmount) : wallet); + @ ensures Company_wallet == \old(((wallet >= matchAmount) && (wallet < (matchAmount + amount))) ? (Company_wallet + matchAmount) : Company_wallet) && wallet == \old(((wallet >= matchAmount) && (wallet < (matchAmount + amount))) ? (wallet - matchAmount) : wallet); + @ ensures assetPreservation(); + @*/ + public static void event_0() { + if (((wallet >= matchAmount) && (wallet < (matchAmount + amount)))) { + int tmp_2 = matchAmount; wallet = wallet - tmp_2;Company_wallet = Company_wallet + tmp_2; // asset transfer + } + } + // behavior + /*@ public normal_behavior + @ requires ( Employee_wallet > 20 * donationSize ) && ( Company_wallet > matchAmount && wallet == 0 ) && ( start_w == matchAmount && donate_w == donationSize ); + @ ensures ( wallet < amount ==> Company_wallet == \old(Company_wallet) ) && ( wallet >= amount ==> Company_wallet == \old(Company_wallet) - matchAmount ); + @ assignable \everything; + @*/ + public static void behavior() { + currentState = -1; + resetDispatch(); + GenStart(); + } + + // GEN_C(Q) for state that does not occur on a cycle + public static void GenStart() { + currentState = Start; + int next_action = computeNextStepEmptyEvents(1); + //@ assume next_action < 0 || (next_action > 0 ? Start_evalConditionFor(next_action) : false); + switch (next_action) { + case 1: + start(start_w); + GenCollect(); + break; + default: break; + } + } + + // GEN_C(Q) for state that does not occur on a cycle + public static void GenEnd() { + currentState = End; + } + + // GEN_C(Q) for initial state of a cycle + public static void GenCollect() { + currentState = Collect; + int op = executeCycleCollect(); + switch(-(op + 1)) { + case 0: + event_0(); + DT_MIN[0] = -1; + DT_MAX[0] = -1; + GenEnd(); + break; + default: break; + } + } + + public static int executeCycleCollect() { + int count = 0; + int op = 1; + int[] stateEvents = new int[] { 0 }; + /*@ loop_invariant 0 <= count <= MAX_ITE_Collect; + @ loop_invariant currentState == Collect; + @ loop_invariant ( 0 <= Employee_wallet <= \old(Employee_wallet) ); + @ loop_invariant ( \old(Employee_wallet) + \old(wallet) == Employee_wallet + wallet ); + @ loop_invariant ( Employee_wallet >= (MAX_ITE_Collect - count) * donationSize ); + @ loop_invariant ( \old(now) <= now <= \old(now) + endTime ); + @ loop_invariant ( 0 < op <= 1 || -2 <= op <= -1 ); + @ assignable wallet, Employee_wallet, now; + @ decreases MAX_ITE_Collect - count; + @*/ + while (count < MAX_ITE_Collect && op > 0) { + switch (op) { + case 1: + donate(donate_w); + break; + default: throw new RuntimeException("Should never be reached."); + } + currentState = Collect; + op = computeNextStep(1, stateEvents); + //@ assume op < 0 || (op > 0 ? Collect_evalConditionFor(op) : false); + count += 1; + } + if (op < 0) { + return op; + } else { + return computeNextStepNoFunctions(stateEvents); + } + } + // auxiliary methods + public final static int computeNextStepNoFunctions(int[] events){ + int entry = minTimeEntry(events); + if (entry == -1) { + return -(events.length + 1); + } else if (DT_MIN[entry] >= now) { + now = DT_MIN[entry]; + } + return -(entry + 1); + } + public final static int computeNextStepEmptyEvents(int nrFct){ + if (nrFct == 0) { + return -1; + } else { + int max_entry = maxTimeEntry(); + int max_time = max_entry == -1 ? now : DT_MAX[max_entry] + 1; + int u_Q = choose(now, max_time); + now = u_Q; + return choose(1,nrFct); + } + } + public final static int computeNextStep(int nrFct, int[] events){ + int w_Q; + int entry = minTimeEntry(events); + int max_entry = maxTimeEntry(); + int max_time = (max_entry == -1 ? now : DT_MAX[max_entry] + 1); + int u_Q = choose(now, max_time); + if (entry == -1) { + w_Q = choose(1,nrFct); + now = u_Q; + return w_Q; + } else { + int dtMaxEntry = DT_MAX[entry]; + int dtMinEntry = DT_MIN[entry]; + if ((dtMinEntry == now) ? true : (dtMaxEntry == now)) { + return -(entry + 1); + } else { + w_Q = choose(0, nrFct); + if (w_Q != 0) { + int timeval = maxSafeTimeIncrement(events); + now = (dtMinEntry < now ? min(dtMinEntry - 1, u_Q) : min(max(timeval-1, now), u_Q)); + return w_Q; + } else { + now = (dtMinEntry < now ? now : dtMinEntry); + return -(entry + 1); + } + } + } + } + /*@ public normal_behavior + @ requires DT_MIN != null && DT_MAX != null & DT_MIN.length == DT_MAX.length; + @ requires events.length <= DT_MIN.length; + @ requires (\forall int i; 0 <= i < events.length; 0 <= events[i] < DT_MIN.length); + @ requires (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] <= DT_MAX[i]); + @ requires now >= 0; + @ ensures \result == -1 || \result >= now; + @ ensures \result == -1 <==> (\forall int i; 0 <= i < events.length; DT_MAX[events[i]] < now ); + @ ensures \result >= now ==> + @ (\exists int i; 0 <= i < events.length; \result == DT_MIN[events[i]] || \result == DT_MAX[events[i]]) + @ && (\forall int i; 0 <= i < events.length; + @ (DT_MIN[events[i]] >= now ==> \result <= DT_MIN[events[i]]) + @ && (DT_MIN[events[i]] < now && DT_MAX[events[i]] >= now ==> \result <= DT_MAX[events[i]])); + @ assignable \strictly_nothing; + @ + @*/ + public /*@ helper @*/ static int maxSafeTimeIncrement(int[] events) { + int res = -1; + /*@ loop_invariant 0 <= j <= events.length; + @ loop_invariant res == -1 || res >= now; + @ loop_invariant res == -1 <==> (\forall int i; 0 <= i < j; DT_MAX[events[i]] < now ); + @ loop_invariant res >= now ==> + @ (\exists int i; 0 <= i < j; (res == DT_MIN[events[i]]) || (res == DT_MAX[events[i]])) + @ && (\forall int i; 0 <= i < j; + @ (DT_MIN[events[i]] >= now ==> res <= DT_MIN[events[i]]) + @ && (DT_MIN[events[i]] < now && DT_MAX[events[i]] >= now ==> res <= DT_MAX[events[i]])); + @ assignable \strictly_nothing; + @ decreases events.length - j; + @*/ + for (int j = 0; j < events.length; j++) { + final int event = events[j]; + if (res == -1 && DT_MAX[event] >= now) { + res = DT_MAX[event]; + } + if (DT_MIN[event] >= now && res > DT_MIN[event]) { + res = DT_MIN[event]; + } else if (DT_MIN[event] < now && DT_MAX[event] >= now && res > DT_MAX[event]) { + res = DT_MAX[event]; + } + } + return res; + } + // while proving we only use the contract and hence have a non-deterministic choice + // executing the implementation chooses a value randomly + /*@ public normal_behavior + @ requires random != null; + @ requires -1 <= lower <= upper; + @ ensures lower <= \result <= upper; + @ assignable \nothing; + */ + private /*@ helper @*/ static int choose(int lower, int upper) { + return random.nextInt(upper + 1 - lower) + lower; + } + /** + * Note: note implementation is deterministic, non-deterministic behavior by underspecification + * in contract only + */ + /*@ public normal_behavior + @ requires DT_MIN != null && DT_MAX != null & DT_MIN.length == DT_MAX.length; + @ requires events.length <= DT_MIN.length; + @ requires (\forall int i; 0 <= i < events.length; 0 <= events[i] < DT_MIN.length); + @ requires (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] <= DT_MAX[i]); + @ ensures -1 <= \result < DT_MIN.length; + @ ensures \result == -1 <==> (\forall int i; 0 <= i < events.length; DT_MAX[events[i]] < now); + @ ensures \result != -1 ==> + @ ( DT_MAX[\result] >= now + @ && (\forall int j; 0 <= j < events.length; + @ ((DT_MIN[events[j]] < now && DT_MAX[events[j]] >= now) ==> DT_MIN[\result] <= DT_MAX[events[j]]) + @ && (DT_MIN[events[j]] >= now ==> DT_MIN[\result] <= DT_MIN[events[j]]) + @ ) + @ && (\exists int j; 0 <= j < events.length; \result == events[j]) + @ ); + @ assignable \strictly_nothing; + @*/ + public static /*@ helper @*/ int minTimeEntry(int[] events) { + if (events.length == 0) { + return -1; + } + int minEvent = -1; + /*@ loop_invariant + @ 0 <= i <= events.length + @ && -1 <= minEvent < DT_MIN.length + @ && (minEvent == -1 ? (\forall int j; 0 <= j < i; DT_MAX[events[j]] < now) : + @ ( DT_MAX[minEvent] >= now + @ && (\forall int j; 0 <= j < i; + @ ((DT_MIN[events[j]] < now && DT_MAX[events[j]] >= now) ==> DT_MIN[minEvent] <= DT_MAX[events[j]]) + @ && (DT_MIN[events[j]] >= now ==> DT_MIN[minEvent] <= DT_MIN[events[j]]) + @ ) + @ && (\exists int j; 0 <= j < i; minEvent == events[j]) ) + @ ); + @ assignable \strictly_nothing; + @ decreases events.length - i; + */ + for (int i = 0; i < events.length; i++) { + if (DT_MAX[events[i]] >= now) { + if (minEvent == -1) { + minEvent = events[i]; + } else if (DT_MIN[events[i]] < now && DT_MAX[events[i]] >= now && DT_MAX[events[i]] < DT_MIN[minEvent]) { + minEvent = events[i]; + } else if (DT_MIN[events[i]] >= now && DT_MIN[minEvent] > DT_MIN[events[i]]) { + minEvent = events[i]; + } + } + } + return minEvent; + } + /** + * Note: note implementation is deterministic, non-deterministic behavior by underspecification + * in contract only + */ + /*@ public normal_behavior + @ requires DT_MAX != null; + @ ensures -1 <= \result < DT_MAX.length; + @ ensures \result != -1 ==> (DT_MAX.length > 0 && DT_MAX[\result] >= now && + @ (\forall int j; 0 <= j < DT_MAX.length; DT_MAX[j] <= DT_MAX[\result])); + @ ensures \result == -1 <==> (\forall int j; 0 <= j < DT_MAX.length; DT_MAX[j] < now); + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int maxTimeEntry() { + if (DT_MAX.length == 0) { + return -1; + } + int maxEntry = -1; + /*@ loop_invariant + @ i >= 0 && i <= DT_MAX.length && + @ -1 <= maxEntry < DT_MAX.length && + @ (maxEntry != -1 ==> (DT_MAX[maxEntry] >= now && ( \forall int j; 0 <= j < i; DT_MAX[maxEntry] >= DT_MAX[j]))) && + @ (maxEntry == -1 <==> ( \forall int j; 0 <= j < i; DT_MAX[j] < now)); + @ assignable \strictly_nothing; + @ decreases DT_MAX.length - i; + */ + for (int i = 0; i < DT_MAX.length; i++) { + if (DT_MAX[i] >= now && (maxEntry == -1 || DT_MAX[i] > DT_MAX[maxEntry])) { + maxEntry = i; + } + } + return maxEntry; + } + /*@ private normal_behavior + @ requires DT_MIN != null && DT_MAX != null && DT_MIN.length == DT_MAX.length; + @ ensures (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] == -1); + @ ensures (\forall int i; 0 <= i < DT_MAX.length; DT_MAX[i] == -1); + @ assignable DT_MIN[*], DT_MAX[*]; + @*/ + private static /*@ helper @*/ void resetDispatch() { + /*@ loop_invariant + @ 0 <= i <= DT_MIN.length + @ && (\forall int j; 0 <= j < i; DT_MIN[j] == -1) + @ && (\forall int j; 0 <= j < i; DT_MAX[j] == -1); + @ assignable DT_MIN[*], DT_MAX[*]; + @ decreases DT_MIN.length - i; + @*/ + for (int i = 0; i < DT_MIN.length; i++) { + DT_MIN[i] = -1; + DT_MAX[i] = -1; + } + } + /*@ public normal_behavior + @ ensures \result == (a <= b ? a : b); + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int min(int a, int b) { + return (a <= b) ? a : b; + } + /*@ public normal_behavior + @ ensures \result == (a >= b ? a : b); + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int max(int a, int b) { + return (a >= b) ? a : b; + } + /*@ public normal_behavior + @ requires (\forall int j; 0 <= j < e.length; e[j] >= 0); + @ ensures e.length > 0 ? ((\forall int j; 0 <= j < e.length; \result >= e[j]) + @ && (\exists int j; 0 <= j < e.length; \result == e[j])) : \result == 0; + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int max(int[] e) { + int max = 0; + /*@ loop_invariant + @ i >= 0 && i <= e.length + @ && (\forall int j; 0 <= j < i; max >= e[j]) + @ && (i>0 ==> (\exists int j; 0 <= j < i; max == e[j])) + @ && (i == 0 ==> max == 0) ; + @ assignable \strictly_nothing; + @ decreases e.length - i; + */ + for (int i = 0; i < e.length; i++) { + if (max < e[i]) { + max = e[i]; + } + } + return max; + } +// evaluating function conditions + + private static boolean start_cond(int w) { + return ((w == matchAmount) && Company_wallet >= w); + } + + private static boolean donate_cond(int w) { + return (true && Employee_wallet >= w); + } + + private static boolean Start_evalConditionFor(int fct) { + switch(fct) { + case 1: return start_cond(start_w); + default: return false; + } + } + + private static boolean Collect_evalConditionFor(int fct) { + switch(fct) { + case 1: return donate_cond(donate_w); + default: return false; + } + } + +} \ No newline at end of file diff --git a/key.ui/examples/case-studies/stipula/src/License.java b/key.ui/examples/case-studies/stipula/src/License.java new file mode 100644 index 00000000000..c66ff3e7d3e --- /dev/null +++ b/key.ui/examples/case-studies/stipula/src/License.java @@ -0,0 +1,487 @@ +import java.util.Random; +public class License { + private static Random random = new Random(); + public final static int Inactive = 0; + public final static int Proposal = 1; + public final static int End = 2; + public final static int Trial = 3; + //@ public invariant -1 <= currentState < 4; + public static int currentState = -1; + //@ public static invariant balance >= 0; + public static int balance; + //@ public static invariant Licensor_balance >= 0; + public static int Licensor_balance; + //@ public static invariant Licensee_balance >= 0; + public static int Licensee_balance; + //@ public static invariant token >= 0; + public static int token; + //@ public static invariant Licensor_token >= 0; + public static int Licensor_token; + //@ public static invariant Licensee_token >= 0; + public static int Licensee_token; + + public static int Licensor; + public static int Licensee; + + //@ public static invariant t_start >= 0; + public static int t_start; + //@ public static invariant t_limit >= 0; + public static int t_limit; + public static int cost; + public static int code; + //@ public static invariant now >= 0; + public static int now = 0; + //@ public static invariant DT_MIN.length == 2; + //@ public static invariant DT_MAX.length == DT_MIN.length && DT_MIN != DT_MAX; + //@ public static invariant (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] <= DT_MAX[i]); + public static int[] DT_MIN = new int[2]; + public static int[] DT_MAX = new int[2]; + + // create unique name by prefixing function name tp parameter name + public static int offerLicense_x; + public static int offerLicense_n; + public static int activateLicense_b; + + //@ public static invariant ( t_start <= t_limit ); + /*@ model two_state static boolean assetPreservation() { + return balance + Licensor_balance + Licensee_balance == \old(balance + Licensor_balance + Licensee_balance) && token + Licensor_token + Licensee_token == \old(token + Licensor_token + Licensee_token); + } */ + // functions of the stipula contract + /*@ public normal_behavior + @ requires (true && Licensor_token >= n); + @ requires n >= 0 && Licensor_token >= n; + @ assignable token, code, Licensor_token, DT_MIN[0], DT_MAX[0]; + @ ensures token == \old(token + n) && code == x && Licensor_token == \old(Licensor_token - n); + @ ensures ( \old(DT_MIN[0] == -1 && DT_MAX[0] == -1) ? + @ DT_MIN[0] == now + t_start && DT_MAX[0] == now + t_start + @ : ( + @ ( DT_MAX[0] == (now + t_start > \old(DT_MAX[0]) ? + @ now + t_start : \old(DT_MAX[0]))) + @ && DT_MIN[0] == \old(DT_MIN[0]) + @ ) + @ ); + @ ensures assetPreservation(); + @*/ + public static void offerLicense(int x, int n) { + int tmp_0 = n; Licensor_token = Licensor_token - tmp_0;token = token + tmp_0; // asset transfer + code = x; + int new_time; + new_time = now + t_start; + if (DT_MIN[0] == -1 && DT_MAX[0] == -1) { + DT_MIN[0] = new_time; + DT_MAX[0] = new_time; + } else if (DT_MAX[0] < new_time) { + DT_MAX[0] = new_time; + } + } + /*@ public normal_behavior + @ requires ((b == cost) && Licensee_balance >= b); + @ requires b >= 0 && Licensee_balance >= b; + @ assignable balance, Licensee_balance, DT_MIN[1], DT_MAX[1]; + @ ensures balance == \old(balance + b) && Licensee_balance == \old(Licensee_balance - b); + @ ensures ( \old(DT_MIN[1] == -1 && DT_MAX[1] == -1) ? + @ DT_MIN[1] == now + t_limit && DT_MAX[1] == now + t_limit + @ : ( + @ ( DT_MAX[1] == (now + t_limit > \old(DT_MAX[1]) ? + @ now + t_limit : \old(DT_MAX[1]))) + @ && DT_MIN[1] == \old(DT_MIN[1]) + @ ) + @ ); + @ ensures assetPreservation(); + @*/ + public static void activateLicense(int b) { + int tmp_1 = b; Licensee_balance = Licensee_balance - tmp_1;balance = balance + tmp_1; // asset transfer + + int new_time; + new_time = now + t_limit; + if (DT_MIN[1] == -1 && DT_MAX[1] == -1) { + DT_MIN[1] = new_time; + DT_MAX[1] = new_time; + } else if (DT_MAX[1] < new_time) { + DT_MAX[1] = new_time; + } + } + /*@ public normal_behavior + @ requires (true); + @ requires balance >= balance && token >= token; + @ assignable balance, token, Licensee_token, Licensor_balance; + @ ensures balance == 0 && token == 0 && Licensee_token == \old(Licensee_token + token) && Licensor_balance == \old(Licensor_balance + balance); + @ ensures assetPreservation(); + @*/ + public static void buy() { + int tmp_2 = balance; balance = balance - tmp_2;Licensor_balance = Licensor_balance + tmp_2; // asset transfer + int tmp_3 = token; token = token - tmp_3;Licensee_token = Licensee_token + tmp_3; // asset transfer + } + // event functions + /*@ public normal_behavior + @ requires token >= token; + @ assignable token, Licensor_token; + @ ensures token == 0 && Licensor_token == \old(Licensor_token + token); + @ ensures token == 0 && Licensor_token == \old(Licensor_token + token); + @ ensures assetPreservation(); + @*/ + public static void event_0() { + int tmp_4 = token; token = token - tmp_4;Licensor_token = Licensor_token + tmp_4; // asset transfer + } + /*@ public normal_behavior + @ requires balance >= balance && token >= token; + @ assignable balance, token, Licensee_balance, Licensor_token; + @ ensures balance == 0 && token == 0 && Licensee_balance == \old(Licensee_balance + balance) && Licensor_token == \old(Licensor_token + token); + @ ensures balance == 0 && token == 0 && Licensee_balance == \old(Licensee_balance + balance) && Licensor_token == \old(Licensor_token + token); + @ ensures assetPreservation(); + @*/ + public static void event_1() { + int tmp_5 = balance; balance = balance - tmp_5;Licensee_balance = Licensee_balance + tmp_5; // asset transfer + int tmp_6 = token; token = token - tmp_6;Licensor_token = Licensor_token + tmp_6; // asset transfer + } + // behavior + /*@ public normal_behavior + @ requires ( Licensor_balance >= 0 && Licensee_balance > 0 && Licensor_token > 0 && Licensee_token == 0 ) && ( Licensor_token == offerLicense_n && Licensee_balance >= activateLicense_b && offerLicense_n >= 0 ) && ( activateLicense_b == cost ) && ( balance == 0 && token == 0 ); + @ requires ( cost >= 0 ); + @ ensures ( (Licensor_balance == \old(Licensor_balance)+cost && Licensor_token == 0 + && Licensee_balance == \old(Licensee_balance)-cost + && Licensee_token == \old(Licensee_token + Licensor_token) + ) || ( + Licensor_balance == \old(Licensor_balance) && + Licensor_token == \old(Licensor_token) && + Licensee_balance == \old(Licensee_balance) && + Licensee_token == \old(Licensee_token) + ) ) && ( currentState == End ); + @ assignable \everything; + @*/ + public static void behavior() { + currentState = -1; + resetDispatch(); + GenInactive(); + } + + // GEN_C(Q) for state that does not occur on a cycle + public static void GenInactive() { + currentState = Inactive; + int next_action = computeNextStepEmptyEvents(1); + //@ assume next_action < 0 || (next_action > 0 ? Inactive_evalConditionFor(next_action) : false); + switch (next_action) { + case 1: + offerLicense(offerLicense_x, offerLicense_n); + GenProposal(); + break; + default: break; + } + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenProposal() { + currentState = Proposal; + int next_action = computeNextStep(1, new int[] { 0 }); + //@ assume next_action < 0 || (next_action > 0 ? Proposal_evalConditionFor(next_action) : false); + switch (next_action) { + case 1: + activateLicense(activateLicense_b); + GenTrial(); + break; + case -1: + event_0(); + DT_MIN[0] = -1; + DT_MAX[0] = -1; + GenEnd(); + break; + default: break; + } + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenEnd() { + currentState = End; + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenTrial() { + currentState = Trial; + int next_action = computeNextStep(1, new int[] { 1 }); + switch (next_action) { + case 1: + buy(); + GenEnd(); + break; + case -2: + event_1(); + DT_MIN[1] = -1; + DT_MAX[1] = -1; + GenEnd(); + break; + default: break; + } + } + + + + // auxiliary methods + public final static int computeNextStepNoFunctions(int[] events){ + int entry = minTimeEntry(events); + if (entry == -1) { + return -(events.length + 1); + } else if (DT_MIN[entry] >= now) { + now = DT_MIN[entry]; + } + return -(entry + 1); + } + public final static int computeNextStepEmptyEvents(int nrFct){ + if (nrFct == 0) { + return -1; + } else { + int max_entry = maxTimeEntry(); + int max_time = max_entry == -1 ? now : DT_MAX[max_entry] + 1; + int u_Q = choose(now, max_time); + now = u_Q; + return choose(1,nrFct); + } + } + public final static int computeNextStep(int nrFct, int[] events){ + int w_Q; + int entry = minTimeEntry(events); + int max_entry = maxTimeEntry(); + int max_time = (max_entry == -1 ? now : DT_MAX[max_entry] + 1); + int u_Q = choose(now, max_time); + if (entry == -1) { + w_Q = choose(1,nrFct); + now = u_Q; + return w_Q; + } else { + int dtMaxEntry = DT_MAX[entry]; + int dtMinEntry = DT_MIN[entry]; + if ((dtMinEntry == now) ? true : (dtMaxEntry == now)) { + return -(entry + 1); + } else { + w_Q = choose(0, nrFct); + if (w_Q != 0) { + int timeval = maxSafeTimeIncrement(events); + now = (dtMinEntry < now ? min(dtMinEntry - 1, u_Q) : min(max(timeval-1, now), u_Q)); + return w_Q; + } else { + now = (dtMinEntry < now ? now : dtMinEntry); + return -(entry + 1); + } + } + } + } + /*@ public normal_behavior + @ requires DT_MIN != null && DT_MAX != null & DT_MIN.length == DT_MAX.length; + @ requires events.length <= DT_MIN.length; + @ requires (\forall int i; 0 <= i < events.length; 0 <= events[i] < DT_MIN.length); + @ requires (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] <= DT_MAX[i]); + @ requires now >= 0; + @ ensures \result == -1 || \result >= now; + @ ensures \result == -1 <==> (\forall int i; 0 <= i < events.length; DT_MAX[events[i]] < now ); + @ ensures \result >= now ==> + @ (\exists int i; 0 <= i < events.length; \result == DT_MIN[events[i]] || \result == DT_MAX[events[i]]) + @ && (\forall int i; 0 <= i < events.length; + @ (DT_MIN[events[i]] >= now ==> \result <= DT_MIN[events[i]]) + @ && (DT_MIN[events[i]] < now && DT_MAX[events[i]] >= now ==> \result <= DT_MAX[events[i]])); + @ assignable \strictly_nothing; + @ + @*/ + public /*@ helper @*/ static int maxSafeTimeIncrement(int[] events) { + int res = -1; + /*@ loop_invariant 0 <= j <= events.length; + @ loop_invariant res == -1 || res >= now; + @ loop_invariant res == -1 <==> (\forall int i; 0 <= i < j; DT_MAX[events[i]] < now ); + @ loop_invariant res >= now ==> + @ (\exists int i; 0 <= i < j; (res == DT_MIN[events[i]]) || (res == DT_MAX[events[i]])) + @ && (\forall int i; 0 <= i < j; + @ (DT_MIN[events[i]] >= now ==> res <= DT_MIN[events[i]]) + @ && (DT_MIN[events[i]] < now && DT_MAX[events[i]] >= now ==> res <= DT_MAX[events[i]])); + @ assignable \strictly_nothing; + @ decreases events.length - j; + @*/ + for (int j = 0; j < events.length; j++) { + final int event = events[j]; + if (res == -1 && DT_MAX[event] >= now) { + res = DT_MAX[event]; + } + if (DT_MIN[event] >= now && res > DT_MIN[event]) { + res = DT_MIN[event]; + } else if (DT_MIN[event] < now && DT_MAX[event] >= now && res > DT_MAX[event]) { + res = DT_MAX[event]; + } + } + return res; + } + // while proving we only use the contract and hence have a non-deterministic choice + // executing the implementation chooses a value randomly + /*@ public normal_behavior + @ requires random != null; + @ requires -1 <= lower <= upper; + @ ensures lower <= \result <= upper; + @ assignable \nothing; + */ + private /*@ helper @*/ static int choose(int lower, int upper) { + return random.nextInt(upper + 1 - lower) + lower; + } + /** + * Note: note implementation is deterministic, non-deterministic behavior by underspecification + * in contract only + */ + /*@ public normal_behavior + @ requires DT_MIN != null && DT_MAX != null & DT_MIN.length == DT_MAX.length; + @ requires events.length <= DT_MIN.length; + @ requires (\forall int i; 0 <= i < events.length; 0 <= events[i] < DT_MIN.length); + @ requires (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] <= DT_MAX[i]); + @ ensures -1 <= \result < DT_MIN.length; + @ ensures \result == -1 <==> (\forall int i; 0 <= i < events.length; DT_MAX[events[i]] < now); + @ ensures \result != -1 ==> + @ ( DT_MAX[\result] >= now + @ && (\forall int j; 0 <= j < events.length; + @ ((DT_MIN[events[j]] < now && DT_MAX[events[j]] >= now) ==> DT_MIN[\result] <= DT_MAX[events[j]]) + @ && (DT_MIN[events[j]] >= now ==> DT_MIN[\result] <= DT_MIN[events[j]]) + @ ) + @ && (\exists int j; 0 <= j < events.length; \result == events[j]) + @ ); + @ assignable \strictly_nothing; + @*/ + public static /*@ helper @*/ int minTimeEntry(int[] events) { + if (events.length == 0) { + return -1; + } + int minEvent = -1; + /*@ loop_invariant + @ 0 <= i <= events.length + @ && -1 <= minEvent < DT_MIN.length + @ && (minEvent == -1 ? (\forall int j; 0 <= j < i; DT_MAX[events[j]] < now) : + @ ( DT_MAX[minEvent] >= now + @ && (\forall int j; 0 <= j < i; + @ ((DT_MIN[events[j]] < now && DT_MAX[events[j]] >= now) ==> DT_MIN[minEvent] <= DT_MAX[events[j]]) + @ && (DT_MIN[events[j]] >= now ==> DT_MIN[minEvent] <= DT_MIN[events[j]]) + @ ) + @ && (\exists int j; 0 <= j < i; minEvent == events[j]) ) + @ ); + @ assignable \strictly_nothing; + @ decreases events.length - i; + */ + for (int i = 0; i < events.length; i++) { + if (DT_MAX[events[i]] >= now) { + if (minEvent == -1) { + minEvent = events[i]; + } else if (DT_MIN[events[i]] < now && DT_MAX[events[i]] >= now && DT_MAX[events[i]] < DT_MIN[minEvent]) { + minEvent = events[i]; + } else if (DT_MIN[events[i]] >= now && DT_MIN[minEvent] > DT_MIN[events[i]]) { + minEvent = events[i]; + } + } + } + return minEvent; + } + /** + * Note: note implementation is deterministic, non-deterministic behavior by underspecification + * in contract only + */ + /*@ public normal_behavior + @ requires DT_MAX != null; + @ ensures -1 <= \result < DT_MAX.length; + @ ensures \result != -1 ==> (DT_MAX.length > 0 && DT_MAX[\result] >= now && + @ (\forall int j; 0 <= j < DT_MAX.length; DT_MAX[j] <= DT_MAX[\result])); + @ ensures \result == -1 <==> (\forall int j; 0 <= j < DT_MAX.length; DT_MAX[j] < now); + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int maxTimeEntry() { + if (DT_MAX.length == 0) { + return -1; + } + int maxEntry = -1; + /*@ loop_invariant + @ i >= 0 && i <= DT_MAX.length && + @ -1 <= maxEntry < DT_MAX.length && + @ (maxEntry != -1 ==> (DT_MAX[maxEntry] >= now && ( \forall int j; 0 <= j < i; DT_MAX[maxEntry] >= DT_MAX[j]))) && + @ (maxEntry == -1 <==> ( \forall int j; 0 <= j < i; DT_MAX[j] < now)); + @ assignable \strictly_nothing; + @ decreases DT_MAX.length - i; + */ + for (int i = 0; i < DT_MAX.length; i++) { + if (DT_MAX[i] >= now && (maxEntry == -1 || DT_MAX[i] > DT_MAX[maxEntry])) { + maxEntry = i; + } + } + return maxEntry; + } + /*@ private normal_behavior + @ requires DT_MIN != null && DT_MAX != null && DT_MIN.length == DT_MAX.length; + @ ensures (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] == -1); + @ ensures (\forall int i; 0 <= i < DT_MAX.length; DT_MAX[i] == -1); + @ assignable DT_MIN[*], DT_MAX[*]; + @*/ + private static /*@ helper @*/ void resetDispatch() { + /*@ loop_invariant + @ 0 <= i <= DT_MIN.length + @ && (\forall int j; 0 <= j < i; DT_MIN[j] == -1) + @ && (\forall int j; 0 <= j < i; DT_MAX[j] == -1); + @ assignable DT_MIN[*], DT_MAX[*]; + @ decreases DT_MIN.length - i; + @*/ + for (int i = 0; i < DT_MIN.length; i++) { + DT_MIN[i] = -1; + DT_MAX[i] = -1; + } + } + /*@ public normal_behavior + @ ensures \result == (a <= b ? a : b); + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int min(int a, int b) { + return (a <= b) ? a : b; + } + /*@ public normal_behavior + @ ensures \result == (a >= b ? a : b); + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int max(int a, int b) { + return (a >= b) ? a : b; + } + /*@ public normal_behavior + @ requires (\forall int j; 0 <= j < e.length; e[j] >= 0); + @ ensures e.length > 0 ? ((\forall int j; 0 <= j < e.length; \result >= e[j]) + @ && (\exists int j; 0 <= j < e.length; \result == e[j])) : \result == 0; + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int max(int[] e) { + int max = 0; + /*@ loop_invariant + @ i >= 0 && i <= e.length + @ && (\forall int j; 0 <= j < i; max >= e[j]) + @ && (i>0 ==> (\exists int j; 0 <= j < i; max == e[j])) + @ && (i == 0 ==> max == 0) ; + @ assignable \strictly_nothing; + @ decreases e.length - i; + */ + for (int i = 0; i < e.length; i++) { + if (max < e[i]) { + max = e[i]; + } + } + return max; + } +// evaluating function conditions + + private static boolean offerLicense_cond(int x, int n) { + return (true && Licensor_token >= n); + } + + private static boolean activateLicense_cond(int b) { + return ((b == cost) && Licensee_balance >= b); + } + + + private static boolean Inactive_evalConditionFor(int fct) { + switch(fct) { + case 1: return offerLicense_cond(offerLicense_x, offerLicense_n); + default: return false; + } + } + + private static boolean Proposal_evalConditionFor(int fct) { + switch(fct) { + case 1: return activateLicense_cond(activateLicense_b); + default: return false; + } + } + + + private static boolean Trial_evalConditionFor(int fct) { + return true; + } +} \ No newline at end of file diff --git a/key.ui/examples/case-studies/stipula/src/LoanForUse.java b/key.ui/examples/case-studies/stipula/src/LoanForUse.java new file mode 100644 index 00000000000..41215b55d4d --- /dev/null +++ b/key.ui/examples/case-studies/stipula/src/LoanForUse.java @@ -0,0 +1,483 @@ +import java.util.Random; +public class LoanForUse { + private static Random random = new Random(); + public final static int Inactive = 0; + public final static int Proposal = 1; + public final static int Consensus = 2; + public final static int Finished = 3; + public final static int End = 4; + //@ public invariant -1 <= currentState < 5; + public static int currentState = -1; + //@ public static invariant code >= 0; + public static int code; + //@ public static invariant Lender_code >= 0; + public static int Lender_code; + //@ public static invariant Borrower_code >= 0; + public static int Borrower_code; + + public static int Lender; + public static int Borrower; + + public static int numLocker; + //@ public static invariant timeLimit >= 0; + public static int timeLimit; + public static int value; + //@ public static invariant now >= 0; + public static int now = 0; + //@ public static invariant DT_MIN.length == 2; + //@ public static invariant DT_MAX.length == DT_MIN.length && DT_MIN != DT_MAX; + //@ public static invariant (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] <= DT_MAX[i]); + public static int[] DT_MIN = new int[2]; + public static int[] DT_MAX = new int[2]; + + // create unique name by prefixing function name tp parameter name + public static int proposal_Locker_num; + public static int proposal_Locker_c; + + + //@ public static invariant ( timeLimit >= 0 && value >= 0 ); + /*@ model two_state static boolean assetPreservation() { + return code + Lender_code + Borrower_code == \old(code + Lender_code + Borrower_code); + } */ + // functions of the stipula contract + /*@ public normal_behavior + @ requires (true && Lender_code >= c); + @ requires c >= 0 && Lender_code >= c; + @ assignable code, Lender_code, numLocker; + @ ensures code == \old(code + c) && Lender_code == \old(Lender_code - c) && numLocker == num; + @ ensures assetPreservation(); + @*/ + public static void proposal_Locker(int num, int c) { + numLocker = num; + int tmp_0 = c; Lender_code = Lender_code - tmp_0;code = code + tmp_0; // asset transfer + } + /*@ public normal_behavior + @ requires (true); + @ assignable \nothing, DT_MIN[0], DT_MAX[0]; + @ ensures true; + @ ensures ( \old(DT_MIN[0] == -1 && DT_MAX[0] == -1) ? + @ DT_MIN[0] == now + timeLimit && DT_MAX[0] == now + timeLimit + @ : ( + @ ( DT_MAX[0] == (now + timeLimit > \old(DT_MAX[0]) ? + @ now + timeLimit : \old(DT_MAX[0]))) + @ && DT_MIN[0] == \old(DT_MIN[0]) + @ ) + @ ); + @ ensures assetPreservation(); + @*/ + public static void declare_Agreement() { + + + int new_time; + new_time = now + timeLimit; + if (DT_MIN[0] == -1 && DT_MAX[0] == -1) { + DT_MIN[0] = new_time; + DT_MAX[0] = new_time; + } else if (DT_MAX[0] < new_time) { + DT_MAX[0] = new_time; + } + } + /*@ public normal_behavior + @ requires (true); + @ requires code >= code; + @ assignable code, Lender_code; + @ ensures code == 0 && Lender_code == \old(Lender_code + code); + @ ensures assetPreservation(); + @*/ + public static void returnB() { + int tmp_1 = code; code = code - tmp_1;Lender_code = Lender_code + tmp_1; // asset transfer + } + /*@ public normal_behavior + @ requires (true); + @ assignable \nothing, DT_MIN[1], DT_MAX[1]; + @ ensures true; + @ ensures ( \old(DT_MIN[1] == -1 && DT_MAX[1] == -1) ? + @ DT_MIN[1] == now + 15 && DT_MAX[1] == now + 15 + @ : ( + @ ( DT_MAX[1] == (now + 15 > \old(DT_MAX[1]) ? + @ now + 15 : \old(DT_MAX[1]))) + @ && DT_MIN[1] == \old(DT_MIN[1]) + @ ) + @ ); + @ ensures assetPreservation(); + @*/ + public static void immediate_Return() { + + int new_time; + new_time = now + 15; + if (DT_MIN[1] == -1 && DT_MAX[1] == -1) { + DT_MIN[1] = new_time; + DT_MAX[1] = new_time; + } else if (DT_MAX[1] < new_time) { + DT_MAX[1] = new_time; + } + } + // event functions + /*@ public normal_behavior + @ requires code >= code; + @ assignable code, Lender_code; + @ ensures code == 0 && Lender_code == \old(Lender_code + code); + @ ensures code == 0 && Lender_code == \old(Lender_code + code); + @ ensures assetPreservation(); + @*/ + public static void event_0() { + + + int tmp_2 = code; code = code - tmp_2;Lender_code = Lender_code + tmp_2; // asset transfer + } + /*@ public normal_behavior + @ requires code >= code; + @ assignable code, Lender_code; + @ ensures code == 0 && Lender_code == \old(Lender_code + code); + @ ensures code == 0 && Lender_code == \old(Lender_code + code); + @ ensures assetPreservation(); + @*/ + public static void event_1() { + + + int tmp_3 = code; code = code - tmp_3;Lender_code = Lender_code + tmp_3; // asset transfer + } + // behavior + /*@ public normal_behavior + @ requires ( proposal_Locker_c >= 0 && code == 0 && Borrower_code == 0 ); + @ ensures ( assetPreservation() ) && ( currentState == Finished ==> (Lender_code == \old(Lender_code) && code == 0) ); + @ assignable \everything; + @*/ + public static void behavior() { + currentState = -1; + resetDispatch(); + GenInactive(); + } + + // GEN_C(Q) for state that does not occur on a cycle + public static void GenInactive() { + currentState = Inactive; + int next_action = computeNextStepEmptyEvents(1); + //@ assume next_action < 0 || (next_action > 0 ? Inactive_evalConditionFor(next_action) : false); + switch (next_action) { + case 1: + proposal_Locker(proposal_Locker_num, proposal_Locker_c); + GenProposal(); + break; + default: break; + } + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenProposal() { + currentState = Proposal; + int next_action = computeNextStepEmptyEvents(1); + switch (next_action) { + case 1: + declare_Agreement(); + GenConsensus(); + break; + default: break; + } + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenConsensus() { + currentState = Consensus; + int next_action = computeNextStep(2, new int[] { 0, 1 }); + switch (next_action) { + case 1: + returnB(); + GenFinished(); + break; + case 2: + immediate_Return(); + GenEnd(); + break; + case -1: + event_0(); + DT_MIN[0] = -1; + DT_MAX[0] = -1; + GenFinished(); + break; + case -2: + event_1(); + DT_MIN[1] = -1; + DT_MAX[1] = -1; + GenFinished(); + break; + default: break; + } + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenFinished() { + currentState = Finished; + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenEnd() { + currentState = End; + } + + + + // auxiliary methods + public final static int computeNextStepNoFunctions(int[] events){ + int entry = minTimeEntry(events); + if (entry == -1) { + return -(events.length + 1); + } else if (DT_MIN[entry] >= now) { + now = DT_MIN[entry]; + } + return -(entry + 1); + } + public final static int computeNextStepEmptyEvents(int nrFct){ + if (nrFct == 0) { + return -1; + } else { + int max_entry = maxTimeEntry(); + int max_time = max_entry == -1 ? now : DT_MAX[max_entry] + 1; + int u_Q = choose(now, max_time); + now = u_Q; + return choose(1,nrFct); + } + } + public final static int computeNextStep(int nrFct, int[] events){ + int w_Q; + int entry = minTimeEntry(events); + int max_entry = maxTimeEntry(); + int max_time = (max_entry == -1 ? now : DT_MAX[max_entry] + 1); + int u_Q = choose(now, max_time); + if (entry == -1) { + w_Q = choose(1,nrFct); + now = u_Q; + return w_Q; + } else { + int dtMaxEntry = DT_MAX[entry]; + int dtMinEntry = DT_MIN[entry]; + if ((dtMinEntry == now) ? true : (dtMaxEntry == now)) { + return -(entry + 1); + } else { + w_Q = choose(0, nrFct); + if (w_Q != 0) { + int timeval = maxSafeTimeIncrement(events); + now = (dtMinEntry < now ? min(dtMinEntry - 1, u_Q) : min(max(timeval-1, now), u_Q)); + return w_Q; + } else { + now = (dtMinEntry < now ? now : dtMinEntry); + return -(entry + 1); + } + } + } + } + /*@ public normal_behavior + @ requires DT_MIN != null && DT_MAX != null & DT_MIN.length == DT_MAX.length; + @ requires events.length <= DT_MIN.length; + @ requires (\forall int i; 0 <= i < events.length; 0 <= events[i] < DT_MIN.length); + @ requires (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] <= DT_MAX[i]); + @ requires now >= 0; + @ ensures \result == -1 || \result >= now; + @ ensures \result == -1 <==> (\forall int i; 0 <= i < events.length; DT_MAX[events[i]] < now ); + @ ensures \result >= now ==> + @ (\exists int i; 0 <= i < events.length; \result == DT_MIN[events[i]] || \result == DT_MAX[events[i]]) + @ && (\forall int i; 0 <= i < events.length; + @ (DT_MIN[events[i]] >= now ==> \result <= DT_MIN[events[i]]) + @ && (DT_MIN[events[i]] < now && DT_MAX[events[i]] >= now ==> \result <= DT_MAX[events[i]])); + @ assignable \strictly_nothing; + @ + @*/ + public /*@ helper @*/ static int maxSafeTimeIncrement(int[] events) { + int res = -1; + /*@ loop_invariant 0 <= j <= events.length; + @ loop_invariant res == -1 || res >= now; + @ loop_invariant res == -1 <==> (\forall int i; 0 <= i < j; DT_MAX[events[i]] < now ); + @ loop_invariant res >= now ==> + @ (\exists int i; 0 <= i < j; (res == DT_MIN[events[i]]) || (res == DT_MAX[events[i]])) + @ && (\forall int i; 0 <= i < j; + @ (DT_MIN[events[i]] >= now ==> res <= DT_MIN[events[i]]) + @ && (DT_MIN[events[i]] < now && DT_MAX[events[i]] >= now ==> res <= DT_MAX[events[i]])); + @ assignable \strictly_nothing; + @ decreases events.length - j; + @*/ + for (int j = 0; j < events.length; j++) { + final int event = events[j]; + if (res == -1 && DT_MAX[event] >= now) { + res = DT_MAX[event]; + } + if (DT_MIN[event] >= now && res > DT_MIN[event]) { + res = DT_MIN[event]; + } else if (DT_MIN[event] < now && DT_MAX[event] >= now && res > DT_MAX[event]) { + res = DT_MAX[event]; + } + } + return res; + } + // while proving we only use the contract and hence have a non-deterministic choice + // executing the implementation chooses a value randomly + /*@ public normal_behavior + @ requires random != null; + @ requires -1 <= lower <= upper; + @ ensures lower <= \result <= upper; + @ assignable \nothing; + */ + private /*@ helper @*/ static int choose(int lower, int upper) { + return random.nextInt(upper + 1 - lower) + lower; + } + /** + * Note: note implementation is deterministic, non-deterministic behavior by underspecification + * in contract only + */ + /*@ public normal_behavior + @ requires DT_MIN != null && DT_MAX != null & DT_MIN.length == DT_MAX.length; + @ requires events.length <= DT_MIN.length; + @ requires (\forall int i; 0 <= i < events.length; 0 <= events[i] < DT_MIN.length); + @ requires (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] <= DT_MAX[i]); + @ ensures -1 <= \result < DT_MIN.length; + @ ensures \result == -1 <==> (\forall int i; 0 <= i < events.length; DT_MAX[events[i]] < now); + @ ensures \result != -1 ==> + @ ( DT_MAX[\result] >= now + @ && (\forall int j; 0 <= j < events.length; + @ ((DT_MIN[events[j]] < now && DT_MAX[events[j]] >= now) ==> DT_MIN[\result] <= DT_MAX[events[j]]) + @ && (DT_MIN[events[j]] >= now ==> DT_MIN[\result] <= DT_MIN[events[j]]) + @ ) + @ && (\exists int j; 0 <= j < events.length; \result == events[j]) + @ ); + @ assignable \strictly_nothing; + @*/ + public static /*@ helper @*/ int minTimeEntry(int[] events) { + if (events.length == 0) { + return -1; + } + int minEvent = -1; + /*@ loop_invariant + @ 0 <= i <= events.length + @ && -1 <= minEvent < DT_MIN.length + @ && (minEvent == -1 ? (\forall int j; 0 <= j < i; DT_MAX[events[j]] < now) : + @ ( DT_MAX[minEvent] >= now + @ && (\forall int j; 0 <= j < i; + @ ((DT_MIN[events[j]] < now && DT_MAX[events[j]] >= now) ==> DT_MIN[minEvent] <= DT_MAX[events[j]]) + @ && (DT_MIN[events[j]] >= now ==> DT_MIN[minEvent] <= DT_MIN[events[j]]) + @ ) + @ && (\exists int j; 0 <= j < i; minEvent == events[j]) ) + @ ); + @ assignable \strictly_nothing; + @ decreases events.length - i; + */ + for (int i = 0; i < events.length; i++) { + if (DT_MAX[events[i]] >= now) { + if (minEvent == -1) { + minEvent = events[i]; + } else if (DT_MIN[events[i]] < now && DT_MAX[events[i]] >= now && DT_MAX[events[i]] < DT_MIN[minEvent]) { + minEvent = events[i]; + } else if (DT_MIN[events[i]] >= now && DT_MIN[minEvent] > DT_MIN[events[i]]) { + minEvent = events[i]; + } + } + } + return minEvent; + } + /** + * Note: note implementation is deterministic, non-deterministic behavior by underspecification + * in contract only + */ + /*@ public normal_behavior + @ requires DT_MAX != null; + @ ensures -1 <= \result < DT_MAX.length; + @ ensures \result != -1 ==> (DT_MAX.length > 0 && DT_MAX[\result] >= now && + @ (\forall int j; 0 <= j < DT_MAX.length; DT_MAX[j] <= DT_MAX[\result])); + @ ensures \result == -1 <==> (\forall int j; 0 <= j < DT_MAX.length; DT_MAX[j] < now); + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int maxTimeEntry() { + if (DT_MAX.length == 0) { + return -1; + } + int maxEntry = -1; + /*@ loop_invariant + @ i >= 0 && i <= DT_MAX.length && + @ -1 <= maxEntry < DT_MAX.length && + @ (maxEntry != -1 ==> (DT_MAX[maxEntry] >= now && ( \forall int j; 0 <= j < i; DT_MAX[maxEntry] >= DT_MAX[j]))) && + @ (maxEntry == -1 <==> ( \forall int j; 0 <= j < i; DT_MAX[j] < now)); + @ assignable \strictly_nothing; + @ decreases DT_MAX.length - i; + */ + for (int i = 0; i < DT_MAX.length; i++) { + if (DT_MAX[i] >= now && (maxEntry == -1 || DT_MAX[i] > DT_MAX[maxEntry])) { + maxEntry = i; + } + } + return maxEntry; + } + /*@ private normal_behavior + @ requires DT_MIN != null && DT_MAX != null && DT_MIN.length == DT_MAX.length; + @ ensures (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] == -1); + @ ensures (\forall int i; 0 <= i < DT_MAX.length; DT_MAX[i] == -1); + @ assignable DT_MIN[*], DT_MAX[*]; + @*/ + private static /*@ helper @*/ void resetDispatch() { + /*@ loop_invariant + @ 0 <= i <= DT_MIN.length + @ && (\forall int j; 0 <= j < i; DT_MIN[j] == -1) + @ && (\forall int j; 0 <= j < i; DT_MAX[j] == -1); + @ assignable DT_MIN[*], DT_MAX[*]; + @ decreases DT_MIN.length - i; + @*/ + for (int i = 0; i < DT_MIN.length; i++) { + DT_MIN[i] = -1; + DT_MAX[i] = -1; + } + } + /*@ public normal_behavior + @ ensures \result == (a <= b ? a : b); + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int min(int a, int b) { + return (a <= b) ? a : b; + } + /*@ public normal_behavior + @ ensures \result == (a >= b ? a : b); + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int max(int a, int b) { + return (a >= b) ? a : b; + } + /*@ public normal_behavior + @ requires (\forall int j; 0 <= j < e.length; e[j] >= 0); + @ ensures e.length > 0 ? ((\forall int j; 0 <= j < e.length; \result >= e[j]) + @ && (\exists int j; 0 <= j < e.length; \result == e[j])) : \result == 0; + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int max(int[] e) { + int max = 0; + /*@ loop_invariant + @ i >= 0 && i <= e.length + @ && (\forall int j; 0 <= j < i; max >= e[j]) + @ && (i>0 ==> (\exists int j; 0 <= j < i; max == e[j])) + @ && (i == 0 ==> max == 0) ; + @ assignable \strictly_nothing; + @ decreases e.length - i; + */ + for (int i = 0; i < e.length; i++) { + if (max < e[i]) { + max = e[i]; + } + } + return max; + } +// evaluating function conditions + + private static boolean proposal_Locker_cond(int num, int c) { + return (true && Lender_code >= c); + } + + + + private static boolean Inactive_evalConditionFor(int fct) { + switch(fct) { + case 1: return proposal_Locker_cond(proposal_Locker_num, proposal_Locker_c); + default: return false; + } + } + + private static boolean Proposal_evalConditionFor(int fct) { + return true; + } + + private static boolean Consensus_evalConditionFor(int fct) { + return true; + } + + +} \ No newline at end of file diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java index db55e752a10..f98795d7648 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/DependencyTracker.java @@ -146,45 +146,44 @@ private List> inputsOfNode(Node n, } } + Set declared = inputsOfRuleApp(ruleApp, n); // record sequent formula inputs - for (PosInOccurrence in : inputsOfRuleApp(ruleApp, n)) { - // Need to find the graph node corresponding to the used sequent formula in the graph. - // Requires knowing the branch it was produced in. - // Try the branch location of this proof step first, then check the previous branches. - BranchLocation loc = n.getBranchLocation(); - int size = loc.size(); - boolean added = false; - for (int i = 0; i <= size; i++) { - TrackedFormula formula = - new TrackedFormula(in.sequentFormula(), loc, in.isInAntec(), - proof.getServices()); - if (graph.containsNode(formula)) { - input.add(new Pair<>(formula, removed.contains(in))); - added = true; - break; - } - if (loc.size() > 0) { - loc = loc.removeLast(); - } - } - if (!added) { - // Normally only the initial proof obligation reaches here. A formula that is - // neither - // produced by a tracked rule nor part of the root sequent means the tracker missed - // some rule applications -- e.g. it was suspended for the duration of a multi-core - // prover run. Degrade gracefully (treat it as an external input) instead of - // throwing, - // so slicing stays usable on a proof that was partly built without tracking. - TrackedFormula formula = - new TrackedFormula(in.sequentFormula(), loc, in.isInAntec(), - proof.getServices()); - input.add(new Pair<>(formula, removed.contains(in))); + for (PosInOccurrence in : declared) { + input.add(new Pair<>(getTrackedFormulaFor(in, n), removed.contains(in))); + } + // take care of formulas that have been removed (actually modified) due to renaming of + // program variables like v#0 by this step even if not part of the declared formulas + // these implicit changes should be attached as effects of the current rule application + // and the formulas as inputs + for (PosInOccurrence removedPio : removed) { + if (!declared.contains(removedPio)) { + input.add(new Pair<>(getTrackedFormulaFor(removedPio, n), true)); } } - return input; } + /** + * Determine the tracked formula for the given occurrence position and node. A formula might + * not be tracked by the graph if it was an initial one. In that case a new node is created and + * returned + * + * @param pio PosInOccurrence of the formula to look for + * @param n the Node of the branch introducing the formula + * @return the TrackedFormula + */ + private TrackedFormula getTrackedFormulaFor(PosInOccurrence pio, Node n) { + // Need to find the graph node corresponding to the used sequent formula in the graph. + // Requires knowing the branch it was produced in. + // Try the branch location of this proof step first, then check the previous branches. + GraphNode gnode = graph.getGraphNode(proof, n.getBranchLocation(), pio); + if (gnode instanceof TrackedFormula trackedFormula) { + return trackedFormula; + } + return new TrackedFormula(pio.sequentFormula(), BranchLocation.ROOT, pio.isInAntec(), + proof.getServices()); + } + /** * Get all formulas removed by the provided rule application, i.e. all formulas not present * in the replacement nodes. @@ -208,19 +207,21 @@ private Set formulasRemovedBy( private Set formulasRemovedBy(Node node) { Set removed = new HashSet<>(); // compare parent sequent to new sequent - Node parent = node.parent(); - if (parent == null) { + if (node.children().isEmpty()) { return removed; } - Sequent seqParent = parent.sequent(); - var seqNew = new IdentityHashSet<>(node.sequent().asList()); - int i = 1; - for (final var parentFormula : seqParent) { - if (!seqNew.contains(parentFormula)) { - removed.add(new PosInOccurrence(parentFormula, PosInTerm.getTopLevel(), - seqParent.numberInAntecedent(i))); + + final Sequent nodeSequent = node.sequent(); + for (final Node child : node.children()) { + final var childSequent = new IdentityHashSet<>(child.sequent().asList()); + int i = 1; + for (final var nodeFormula : nodeSequent) { + boolean inAntec = nodeSequent.numberInAntecedent(i); + if (!childSequent.contains(nodeFormula)) { + removed.add(new PosInOccurrence(nodeFormula, PosInTerm.getTopLevel(), inAntec)); + } + i++; } - i++; } return removed; } @@ -406,6 +407,9 @@ public void trackNode(Node n) { // record removed (replaced) input formulas // (these are the same for each new branch) + // at the moment yes as renaming (\addprogvars) only used + // by taclets with one goal, below method over-approximates + // in other use cases Set removed = formulasRemovedBy(n); // inputs: (graph node, whether that graph node was replaced) diff --git a/keyext.slicing/src/test/java/org/key_project/slicing/IssueRenamingTest.java b/keyext.slicing/src/test/java/org/key_project/slicing/IssueRenamingTest.java new file mode 100644 index 00000000000..5b0d8383d45 --- /dev/null +++ b/keyext.slicing/src/test/java/org/key_project/slicing/IssueRenamingTest.java @@ -0,0 +1,48 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package org.key_project.slicing; + +import java.nio.file.Path; + +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.proof.io.ProblemLoaderControl; +import de.uka.ilkd.key.settings.GeneralSettings; + +import org.key_project.util.helper.FindResources; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.assertTrue; + +public class IssueRenamingTest { + public static final Path testCaseDirectory = FindResources.getTestCasesDirectory(); + + @Test + void loadsAndSlicesCorrectly() throws Exception { + GeneralSettings.noPruningClosed = false; + + var file = testCaseDirectory.resolve( + "issues/renaming/Bet_behavior.proof.gz"); + var env = KeYEnvironment.load(file); + var proof = env.getLoadedProof(); + var tracker = new DependencyTracker(proof); + env.getProofControl().startAutoMode(proof, proof.openEnabledGoals()); + env.getProofControl().waitWhileAutoMode(); + assertTrue(proof.closed()); + + var results = tracker.analyze(true, false); + + ProblemLoaderControl control = new DefaultUserInterfaceControl(); + SlicingProofReplayer replayer = SlicingProofReplayer + .constructSlicer(control, proof, results, env.getUi()); + var newFile = replayer.slice(); + var env2 = KeYEnvironment.load(newFile); + var proof2 = env2.getLoadedProof(); + assertTrue(proof2.closed()); + env.dispose(); + env2.dispose(); + GeneralSettings.noPruningClosed = true; + } +} diff --git a/keyext.slicing/src/test/resources/testcase/issues/renaming/Bet.java b/keyext.slicing/src/test/resources/testcase/issues/renaming/Bet.java new file mode 100644 index 00000000000..981ebd7c6af --- /dev/null +++ b/keyext.slicing/src/test/resources/testcase/issues/renaming/Bet.java @@ -0,0 +1,515 @@ +import java.util.Random; +public class Bet { + private static Random random = new Random(); + public final static int Init = 0; + public final static int First = 1; + public final static int Fail = 2; + public final static int Run = 3; + public final static int End = 4; + //@ public invariant -1 <= currentState < 5; + public static int currentState = -1; + //@ public static invariant wallet1 >= 0; + public static int wallet1; + //@ public static invariant Better1_wallet1 >= 0; + public static int Better1_wallet1; + //@ public static invariant Better2_wallet1 >= 0; + public static int Better2_wallet1; + //@ public static invariant DataProvider_wallet1 >= 0; + public static int DataProvider_wallet1; + //@ public static invariant wallet2 >= 0; + public static int wallet2; + //@ public static invariant Better1_wallet2 >= 0; + public static int Better1_wallet2; + //@ public static invariant Better2_wallet2 >= 0; + public static int Better2_wallet2; + //@ public static invariant DataProvider_wallet2 >= 0; + public static int DataProvider_wallet2; + + public static int Better1; + public static int Better2; + public static int DataProvider; + + public static int val1; + public static int val2; + public static int event; + public static int amount; + //@ public static invariant t_before >= 0; + public static int t_before; + //@ public static invariant t_after >= 0; + public static int t_after; + //@ public static invariant now >= 0; + public static int now = 0; + //@ public static invariant DT_MIN.length == 2; + //@ public static invariant DT_MAX.length == DT_MIN.length && DT_MIN != DT_MAX; + //@ public static invariant (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] <= DT_MAX[i]); + public static int[] DT_MIN = new int[2]; + public static int[] DT_MAX = new int[2]; + + // create unique name by prefixing function name tp parameter name + public static int place_bet_x; + public static int place_bet_h; + // create unique name by prefixing function name tp parameter name + public static int place_bet2_x; + public static int place_bet2_h; + // create unique name by prefixing function name tp parameter name + public static int data_x, data_z; + //@ public static invariant ( 0 <= t_before < t_after && amount > 0 ); + /*@ model two_state static boolean assetPreservation() { + return wallet1 + Better1_wallet1 + Better2_wallet1 + DataProvider_wallet1 == \old(wallet1 + Better1_wallet1 + Better2_wallet1 + DataProvider_wallet1) && wallet2 + Better1_wallet2 + Better2_wallet2 + DataProvider_wallet2 == \old(wallet2 + Better1_wallet2 + Better2_wallet2 + DataProvider_wallet2); + } */ + // functions of the stipula contract + /*@ public normal_behavior + @ requires ((h == amount) && Better1_wallet1 >= h); + @ requires h >= 0 && Better1_wallet1 >= h; + @ assignable wallet1, val1, Better1_wallet1, DT_MIN[0], DT_MAX[0]; + @ ensures wallet1 == \old(wallet1 + h) && val1 == x && Better1_wallet1 == \old(Better1_wallet1 - h); + @ ensures ( \old(DT_MIN[0] == -1 && DT_MAX[0] == -1) ? + @ DT_MIN[0] == now + t_before && DT_MAX[0] == now + t_before + @ : ( + @ ( DT_MAX[0] == (now + t_before > \old(DT_MAX[0]) ? + @ now + t_before : \old(DT_MAX[0]))) + @ && DT_MIN[0] == \old(DT_MIN[0]) + @ ) + @ ); + @ ensures assetPreservation(); + @*/ + public static void place_bet(int x, int h) { + int tmp_0 = h; Better1_wallet1 = Better1_wallet1 - tmp_0;wallet1 = wallet1 + tmp_0; // asset transfer + val1 = x; + int new_time; + new_time = now + t_before; + if (DT_MIN[0] == -1 && DT_MAX[0] == -1) { + DT_MIN[0] = new_time; + DT_MAX[0] = new_time; + } else if (DT_MAX[0] < new_time) { + DT_MAX[0] = new_time; + } + } + /*@ public normal_behavior + @ requires ((h == amount) && Better2_wallet2 >= h); + @ requires h >= 0 && Better2_wallet2 >= h; + @ assignable wallet2, val2, Better2_wallet2, DT_MIN[1], DT_MAX[1]; + @ ensures wallet2 == \old(wallet2 + h) && val2 == x && Better2_wallet2 == \old(Better2_wallet2 - h); + @ ensures ( \old(DT_MIN[1] == -1 && DT_MAX[1] == -1) ? + @ DT_MIN[1] == now + t_after && DT_MAX[1] == now + t_after + @ : ( + @ ( DT_MAX[1] == (now + t_after > \old(DT_MAX[1]) ? + @ now + t_after : \old(DT_MAX[1]))) + @ && DT_MIN[1] == \old(DT_MIN[1]) + @ ) + @ ); + @ ensures assetPreservation(); + @*/ + public static void place_bet2(int x, int h) { + int tmp_1 = h; Better2_wallet2 = Better2_wallet2 - tmp_1;wallet2 = wallet2 + tmp_1; // asset transfer + val2 = x; + int new_time; + new_time = now + t_after; + if (DT_MIN[1] == -1 && DT_MAX[1] == -1) { + DT_MIN[1] = new_time; + DT_MAX[1] = new_time; + } else if (DT_MAX[1] < new_time) { + DT_MAX[1] = new_time; + } + } + /*@ public normal_behavior + @ requires ((x == event)); + @ assignable wallet2, wallet1, Better1_wallet2, Better1_wallet1, Better2_wallet1, DataProvider_wallet1, DataProvider_wallet2, Better2_wallet2; + @ ensures wallet2 == \old(((z == val1) && (z == val2)) ? 0 : (((z == val1) && (z != val2)) ? 0 : (((z != val1) && (z == val2)) ? 0 : 0))) && wallet1 == \old(((z == val1) && (z == val2)) ? 0 : (((z == val1) && (z != val2)) ? 0 : (((z != val1) && (z == val2)) ? 0 : 0))) && Better1_wallet2 == \old(((z == val1) && (z == val2)) ? Better1_wallet2 : (((z == val1) && (z != val2)) ? (Better1_wallet2 + wallet2) : Better1_wallet2)) && Better1_wallet1 == \old(((z == val1) && (z == val2)) ? (Better1_wallet1 + wallet1) : (((z == val1) && (z != val2)) ? (Better1_wallet1 + wallet1) : Better1_wallet1)) && Better2_wallet1 == \old(((z == val1) && (z == val2)) ? Better2_wallet1 : (((z == val1) && (z != val2)) ? Better2_wallet1 : (((z != val1) && (z == val2)) ? (Better2_wallet1 + wallet1) : Better2_wallet1))) && DataProvider_wallet1 == \old(((z == val1) && (z == val2)) ? DataProvider_wallet1 : (((z == val1) && (z != val2)) ? DataProvider_wallet1 : (((z != val1) && (z == val2)) ? DataProvider_wallet1 : (DataProvider_wallet1 + wallet1)))) && DataProvider_wallet2 == \old(((z == val1) && (z == val2)) ? DataProvider_wallet2 : (((z == val1) && (z != val2)) ? DataProvider_wallet2 : (((z != val1) && (z == val2)) ? DataProvider_wallet2 : (DataProvider_wallet2 + wallet2)))) && Better2_wallet2 == \old(((z == val1) && (z == val2)) ? (Better2_wallet2 + wallet2) : (((z == val1) && (z != val2)) ? Better2_wallet2 : (((z != val1) && (z == val2)) ? (Better2_wallet2 + wallet2) : Better2_wallet2))); + @ ensures assetPreservation(); + @*/ + public static void data(int x, int z) { + if (((z == val1) && (z == val2))) { + int tmp_2 = wallet1; wallet1 = wallet1 - tmp_2;Better1_wallet1 = Better1_wallet1 + tmp_2; // asset transfer +int tmp_3 = wallet2; wallet2 = wallet2 - tmp_3;Better2_wallet2 = Better2_wallet2 + tmp_3; // asset transfer + } else { + if (((z == val1) && (z != val2))) { + int tmp_4 = wallet2; wallet2 = wallet2 - tmp_4;Better1_wallet2 = Better1_wallet2 + tmp_4; // asset transfer +int tmp_5 = wallet1; wallet1 = wallet1 - tmp_5;Better1_wallet1 = Better1_wallet1 + tmp_5; // asset transfer + } else { + if (((z != val1) && (z == val2))) { + int tmp_6 = wallet1; wallet1 = wallet1 - tmp_6;Better2_wallet1 = Better2_wallet1 + tmp_6; // asset transfer +int tmp_7 = wallet2; wallet2 = wallet2 - tmp_7;Better2_wallet2 = Better2_wallet2 + tmp_7; // asset transfer + } else { + int tmp_8 = wallet2; wallet2 = wallet2 - tmp_8;DataProvider_wallet2 = DataProvider_wallet2 + tmp_8; // asset transfer +int tmp_9 = wallet1; wallet1 = wallet1 - tmp_9;DataProvider_wallet1 = DataProvider_wallet1 + tmp_9; // asset transfer + } + } + } + } + // event functions + /*@ public normal_behavior + @ requires wallet1 >= wallet1; + @ assignable wallet1, Better1_wallet1; + @ ensures wallet1 == 0 && Better1_wallet1 == \old(Better1_wallet1 + wallet1); + @ ensures wallet1 == 0 && Better1_wallet1 == \old(Better1_wallet1 + wallet1); + @ ensures assetPreservation(); + @*/ + public static void event_0() { + int tmp_10 = wallet1; wallet1 = wallet1 - tmp_10;Better1_wallet1 = Better1_wallet1 + tmp_10; // asset transfer + } + /*@ public normal_behavior + @ requires wallet1 >= wallet1 && wallet2 >= wallet2; + @ assignable wallet2, wallet1, Better1_wallet1, Better2_wallet2; + @ ensures wallet2 == 0 && wallet1 == 0 && Better1_wallet1 == \old(Better1_wallet1 + wallet1) && Better2_wallet2 == \old(Better2_wallet2 + wallet2); + @ ensures wallet2 == 0 && wallet1 == 0 && Better1_wallet1 == \old(Better1_wallet1 + wallet1) && Better2_wallet2 == \old(Better2_wallet2 + wallet2); + @ ensures assetPreservation(); + @*/ + public static void event_1() { + int tmp_11 = wallet1; wallet1 = wallet1 - tmp_11;Better1_wallet1 = Better1_wallet1 + tmp_11; // asset transfer + int tmp_12 = wallet2; wallet2 = wallet2 - tmp_12;Better2_wallet2 = Better2_wallet2 + tmp_12; // asset transfer + } + // behavior + /*@ public normal_behavior + @ requires ( wallet1 == 0 && wallet2 == 0 ); + @ ensures ( assetPreservation() ) && ( currentState == Fail ==> (wallet1 == 0 && wallet2 == 0 && Better1_wallet1==\old(Better1_wallet1) && Better1_wallet2==\old(Better1_wallet2) && Better2_wallet1==\old(Better2_wallet1) && Better2_wallet2==\old(Better2_wallet2)) ); + @ assignable \everything; + @*/ + public static void behavior() { + currentState = -1; + resetDispatch(); + GenInit(); + } + + // GEN_C(Q) for state that does not occur on a cycle + public static void GenInit() { + currentState = Init; + int next_action = computeNextStepEmptyEvents(1); + //@ assume next_action < 0 || (next_action > 0 ? Init_evalConditionFor(next_action) : false); + switch (next_action) { + case 1: + place_bet(place_bet_x, place_bet_h); + GenFirst(); + break; + default: break; + } + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenFirst() { + currentState = First; + int next_action = computeNextStep(1, new int[] { 0 }); + //@ assume next_action < 0 || (next_action > 0 ? First_evalConditionFor(next_action) : false); + switch (next_action) { + case 1: + place_bet2(place_bet2_x, place_bet2_h); + GenRun(); + break; + case -1: + event_0(); + DT_MIN[0] = -1; + DT_MAX[0] = -1; + GenFail(); + break; + default: break; + } + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenFail() { + currentState = Fail; + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenRun() { + currentState = Run; + int next_action = computeNextStep(1, new int[] { 1 }); + //@ assume next_action < 0 || (next_action > 0 ? Run_evalConditionFor(next_action) : false); + switch (next_action) { + case 1: + data(data_x, data_z); + GenEnd(); + break; + case -2: + event_1(); + DT_MIN[1] = -1; + DT_MAX[1] = -1; + GenFail(); + break; + default: break; + } + } + // GEN_C(Q) for state that does not occur on a cycle + public static void GenEnd() { + currentState = End; + } + + + + // auxiliary methods + public final static int computeNextStepNoFunctions(int[] events){ + int entry = minTimeEntry(events); + if (entry == -1) { + return -(events.length + 1); + } else if (DT_MIN[entry] >= now) { + now = DT_MIN[entry]; + } + return -(entry + 1); + } + public final static int computeNextStepEmptyEvents(int nrFct){ + if (nrFct == 0) { + return -1; + } else { + int max_entry = maxTimeEntry(); + int max_time = max_entry == -1 ? now : DT_MAX[max_entry] + 1; + int u_Q = choose(now, max_time); + now = u_Q; + return choose(1,nrFct); + } + } + public final static int computeNextStep(int nrFct, int[] events){ + int w_Q; + int entry = minTimeEntry(events); + int max_entry = maxTimeEntry(); + int max_time = (max_entry == -1 ? now : DT_MAX[max_entry] + 1); + int u_Q = choose(now, max_time); + if (entry == -1) { + w_Q = choose(1,nrFct); + now = u_Q; + return w_Q; + } else { + int dtMaxEntry = DT_MAX[entry]; + int dtMinEntry = DT_MIN[entry]; + if ((dtMinEntry == now) ? true : (dtMaxEntry == now)) { + return -(entry + 1); + } else { + w_Q = choose(0, nrFct); + if (w_Q != 0) { + int timeval = maxSafeTimeIncrement(events); + now = (dtMinEntry < now ? min(dtMinEntry - 1, u_Q) : min(max(timeval-1, now), u_Q)); + return w_Q; + } else { + now = (dtMinEntry < now ? now : dtMinEntry); + return -(entry + 1); + } + } + } + } + /*@ public normal_behavior + @ requires DT_MIN != null && DT_MAX != null & DT_MIN.length == DT_MAX.length; + @ requires events.length <= DT_MIN.length; + @ requires (\forall int i; 0 <= i < events.length; 0 <= events[i] < DT_MIN.length); + @ requires (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] <= DT_MAX[i]); + @ requires now >= 0; + @ ensures \result == -1 || \result >= now; + @ ensures \result == -1 <==> (\forall int i; 0 <= i < events.length; DT_MAX[events[i]] < now ); + @ ensures \result >= now ==> + @ (\exists int i; 0 <= i < events.length; \result == DT_MIN[events[i]] || \result == DT_MAX[events[i]]) + @ && (\forall int i; 0 <= i < events.length; + @ (DT_MIN[events[i]] >= now ==> \result <= DT_MIN[events[i]]) + @ && (DT_MIN[events[i]] < now && DT_MAX[events[i]] >= now ==> \result <= DT_MAX[events[i]])); + @ assignable \strictly_nothing; + @ + @*/ + public /*@ helper @*/ static int maxSafeTimeIncrement(int[] events) { + int res = -1; + /*@ loop_invariant 0 <= j <= events.length; + @ loop_invariant res == -1 || res >= now; + @ loop_invariant res == -1 <==> (\forall int i; 0 <= i < j; DT_MAX[events[i]] < now ); + @ loop_invariant res >= now ==> + @ (\exists int i; 0 <= i < j; (res == DT_MIN[events[i]]) || (res == DT_MAX[events[i]])) + @ && (\forall int i; 0 <= i < j; + @ (DT_MIN[events[i]] >= now ==> res <= DT_MIN[events[i]]) + @ && (DT_MIN[events[i]] < now && DT_MAX[events[i]] >= now ==> res <= DT_MAX[events[i]])); + @ assignable \strictly_nothing; + @ decreases events.length - j; + @*/ + for (int j = 0; j < events.length; j++) { + final int event = events[j]; + if (res == -1 && DT_MAX[event] >= now) { + res = DT_MAX[event]; + } + if (DT_MIN[event] >= now && res > DT_MIN[event]) { + res = DT_MIN[event]; + } else if (DT_MIN[event] < now && DT_MAX[event] >= now && res > DT_MAX[event]) { + res = DT_MAX[event]; + } + } + return res; + } + // while proving we only use the contract and hence have a non-deterministic choice + // executing the implementation chooses a value randomly + /*@ public normal_behavior + @ requires random != null; + @ requires -1 <= lower <= upper; + @ ensures lower <= \result <= upper; + @ assignable \nothing; + */ + private /*@ helper @*/ static int choose(int lower, int upper) { + return random.nextInt(upper + 1 - lower) + lower; + } + /** + * Note: note implementation is deterministic, non-deterministic behavior by underspecification + * in contract only + */ + /*@ public normal_behavior + @ requires DT_MIN != null && DT_MAX != null & DT_MIN.length == DT_MAX.length; + @ requires events.length <= DT_MIN.length; + @ requires (\forall int i; 0 <= i < events.length; 0 <= events[i] < DT_MIN.length); + @ requires (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] <= DT_MAX[i]); + @ ensures -1 <= \result < DT_MIN.length; + @ ensures \result == -1 <==> (\forall int i; 0 <= i < events.length; DT_MAX[events[i]] < now); + @ ensures \result != -1 ==> + @ ( DT_MAX[\result] >= now + @ && (\forall int j; 0 <= j < events.length; + @ ((DT_MIN[events[j]] < now && DT_MAX[events[j]] >= now) ==> DT_MIN[\result] <= DT_MAX[events[j]]) + @ && (DT_MIN[events[j]] >= now ==> DT_MIN[\result] <= DT_MIN[events[j]]) + @ ) + @ && (\exists int j; 0 <= j < events.length; \result == events[j]) + @ ); + @ assignable \strictly_nothing; + @*/ + public static /*@ helper @*/ int minTimeEntry(int[] events) { + if (events.length == 0) { + return -1; + } + int minEvent = -1; + /*@ loop_invariant + @ 0 <= i <= events.length + @ && -1 <= minEvent < DT_MIN.length + @ && (minEvent == -1 ? (\forall int j; 0 <= j < i; DT_MAX[events[j]] < now) : + @ ( DT_MAX[minEvent] >= now + @ && (\forall int j; 0 <= j < i; + @ ((DT_MIN[events[j]] < now && DT_MAX[events[j]] >= now) ==> DT_MIN[minEvent] <= DT_MAX[events[j]]) + @ && (DT_MIN[events[j]] >= now ==> DT_MIN[minEvent] <= DT_MIN[events[j]]) + @ ) + @ && (\exists int j; 0 <= j < i; minEvent == events[j]) ) + @ ); + @ assignable \strictly_nothing; + @ decreases events.length - i; + */ + for (int i = 0; i < events.length; i++) { + if (DT_MAX[events[i]] >= now) { + if (minEvent == -1) { + minEvent = events[i]; + } else if (DT_MIN[events[i]] < now && DT_MAX[events[i]] >= now && DT_MAX[events[i]] < DT_MIN[minEvent]) { + minEvent = events[i]; + } else if (DT_MIN[events[i]] >= now && DT_MIN[minEvent] > DT_MIN[events[i]]) { + minEvent = events[i]; + } + } + } + return minEvent; + } + /** + * Note: note implementation is deterministic, non-deterministic behavior by underspecification + * in contract only + */ + /*@ public normal_behavior + @ requires DT_MAX != null; + @ ensures -1 <= \result < DT_MAX.length; + @ ensures \result != -1 ==> (DT_MAX.length > 0 && DT_MAX[\result] >= now && + @ (\forall int j; 0 <= j < DT_MAX.length; DT_MAX[j] <= DT_MAX[\result])); + @ ensures \result == -1 <==> (\forall int j; 0 <= j < DT_MAX.length; DT_MAX[j] < now); + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int maxTimeEntry() { + if (DT_MAX.length == 0) { + return -1; + } + int maxEntry = -1; + /*@ loop_invariant + @ i >= 0 && i <= DT_MAX.length && + @ -1 <= maxEntry < DT_MAX.length && + @ (maxEntry != -1 ==> (DT_MAX[maxEntry] >= now && ( \forall int j; 0 <= j < i; DT_MAX[maxEntry] >= DT_MAX[j]))) && + @ (maxEntry == -1 <==> ( \forall int j; 0 <= j < i; DT_MAX[j] < now)); + @ assignable \strictly_nothing; + @ decreases DT_MAX.length - i; + */ + for (int i = 0; i < DT_MAX.length; i++) { + if (DT_MAX[i] >= now && (maxEntry == -1 || DT_MAX[i] > DT_MAX[maxEntry])) { + maxEntry = i; + } + } + return maxEntry; + } + /*@ private normal_behavior + @ requires DT_MIN != null && DT_MAX != null && DT_MIN.length == DT_MAX.length; + @ ensures (\forall int i; 0 <= i < DT_MIN.length; DT_MIN[i] == -1); + @ ensures (\forall int i; 0 <= i < DT_MAX.length; DT_MAX[i] == -1); + @ assignable DT_MIN[*], DT_MAX[*]; + @*/ + private static /*@ helper @*/ void resetDispatch() { + /*@ loop_invariant + @ 0 <= i <= DT_MIN.length + @ && (\forall int j; 0 <= j < i; DT_MIN[j] == -1) + @ && (\forall int j; 0 <= j < i; DT_MAX[j] == -1); + @ assignable DT_MIN[*], DT_MAX[*]; + @ decreases DT_MIN.length - i; + @*/ + for (int i = 0; i < DT_MIN.length; i++) { + DT_MIN[i] = -1; + DT_MAX[i] = -1; + } + } + /*@ public normal_behavior + @ ensures \result == (a <= b ? a : b); + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int min(int a, int b) { + return (a <= b) ? a : b; + } + /*@ public normal_behavior + @ ensures \result == (a >= b ? a : b); + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int max(int a, int b) { + return (a >= b) ? a : b; + } + /*@ public normal_behavior + @ requires (\forall int j; 0 <= j < e.length; e[j] >= 0); + @ ensures e.length > 0 ? ((\forall int j; 0 <= j < e.length; \result >= e[j]) + @ && (\exists int j; 0 <= j < e.length; \result == e[j])) : \result == 0; + @ assignable \strictly_nothing; + */ + public static /*@ helper @*/ int max(int[] e) { + int max = 0; + /*@ loop_invariant + @ i >= 0 && i <= e.length + @ && (\forall int j; 0 <= j < i; max >= e[j]) + @ && (i>0 ==> (\exists int j; 0 <= j < i; max == e[j])) + @ && (i == 0 ==> max == 0) ; + @ assignable \strictly_nothing; + @ decreases e.length - i; + */ + for (int i = 0; i < e.length; i++) { + if (max < e[i]) { + max = e[i]; + } + } + return max; + } +// evaluating function conditions + + private static boolean place_bet_cond(int x, int h) { + return ((h == amount) && Better1_wallet1 >= h); + } + + private static boolean place_bet2_cond(int x, int h) { + return ((h == amount) && Better2_wallet2 >= h); + } + + private static boolean data_cond(int x, int z) { + return ((x == event)); + } + + private static boolean Init_evalConditionFor(int fct) { + switch(fct) { + case 1: return place_bet_cond(place_bet_x, place_bet_h); + default: return false; + } + } + + private static boolean First_evalConditionFor(int fct) { + switch(fct) { + case 1: return place_bet2_cond(place_bet2_x, place_bet2_h); + default: return false; + } + } + + + private static boolean Run_evalConditionFor(int fct) { + switch(fct) { + case 1: return data_cond(data_x, data_z); + default: return false; + } + } + +} \ No newline at end of file diff --git a/keyext.slicing/src/test/resources/testcase/issues/renaming/Bet_behavior.proof.gz b/keyext.slicing/src/test/resources/testcase/issues/renaming/Bet_behavior.proof.gz new file mode 100644 index 00000000000..424a98606e6 Binary files /dev/null and b/keyext.slicing/src/test/resources/testcase/issues/renaming/Bet_behavior.proof.gz differ