\settings {
"#Proof-Settings-Config-File
#Tue Jan 16 15:16:44 CET 2007
[General]SoundNotification=false
[DecisionProcedure]SmtBenchmarkArchiving=false
[View]FontIndex=4
[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_EXPAND
[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_NONE
[SimultaneousUpdateSimplifier]DeleteEffectLessLocations=false
[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE
[General]SuggestiveVarNames=false
[View]ShowWholeTaclet=false
[General]ProofAssistant=false
[View]MaxTooltipLines=40
[General]DnDDirectionSensitive=false
[SimultaneousUpdateSimplifier]EagerSimplification=false
[General]StupidMode=true
[Strategy]MaximumNumberOfAutomaticApplications=10000
[Libraries]Default=acc.key-false, stringRules.key-false, deprecatedRules.key-false
[StrategyProperty]QUERY_OPTIONS_KEY=QUERY_EXPAND
[Choice]DefaultChoices=testGeneration-testGeneration\:testOff , transactions-transactions\:transactionsOff , programRules-programRules\:Java , transactionsPolicy-transactionsPolicy\:noAbortTransaction , initialisation-initialisation\:disableStaticInitialisation , throughout-throughout\:toutOff , transactionAbort-transactionAbort\:abortOn , intRules-intRules\:arithmeticSemanticsIgnoringOF , assertions-assertions\:on , nullPointerPolicy-nullPointerPolicy\:nullCheck
[DecisionProcedure]SmtZipProblemDir=false
[Model]Source=1
[Choice]Choices=transactions-transactions\:transactionsOff-transactions\:transactionsOn , testGeneration-testGeneration\:testOn-testGeneration\:testOff , programRules-programRules\:ODL-programRules\:Java , transactionsPolicy-transactionsPolicy\:abortTransaction-transactionsPolicy\:noAbortTransaction , transactionAbort-transactionAbort\:abortOff-transactionAbort\:abortOn , throughout-throughout\:toutOff-throughout\:toutOn , initialisation-initialisation\:disableStaticInitialisation-initialisation\:enableStaticInitialisation , intRules-intRules\:arithmeticSemanticsCheckingOF-intRules\:javaSemantics-intRules\:arithmeticSemanticsIgnoringOF , assertions-assertions\:safe-assertions\:off-assertions\:on , nullPointerPolicy-nullPointerPolicy\:noNullCheck-nullPointerPolicy\:nullCheck
[DecisionProcedure]SmtUseQuantifiers=true
[DecisionProcedure]=YICES
[General]OuterRenaming=false
[Strategy]ActiveStrategy=JavaCardDLStrategy
"
}

//Example from page 339
//comments on the problem section
//line 1   : definition of   balance@pre
//line 2   : precondition
//line 3-4 : invariant. \phi in Template 5
//line 5   : {self.balance:=l_balance(self)} is
//            the anonymizing update 
//line 6   : postcondition
//line 7   : anonymizing update 
//line 8-9 : invariant
//

\javaSource "paycardChapt8";

\functions {
  int balance@pre(PayCard);
  int l_balance(PayCard);
  PayCard self;
  boolean created(PayCard);
}

\programVariables {
  int amount;
}
\problem {
     \forall PayCard pc; 
       balance@pre(pc) = pc.balance@(PayCard)
   &    self.balance@(PayCard)
      + amount
     <  self.limit@(PayCard)
   & amount >= 0
   & \forall PayCard pc; 
       (   pc.<created>@(java.lang.Object) = TRUE
        ->   0 <= pc.balance@(PayCard)
           & pc.balance@(PayCard) <= pc.limit@(PayCard))
   &   {self.balance@(PayCard):=l_balance(self)}
         self.balance@(PayCard)
     = balance@pre(self) + amount
-> {self.balance@(PayCard):=l_balance(self)}
     \forall PayCard pc; 
       (   pc.<created>@(java.lang.Object) = TRUE
        ->   0 <= pc.balance@(PayCard)
           & pc.balance@(PayCard) <= pc.limit@(PayCard))

}

\proof {
(keyLog "0" (keyUser "pschmitt" ) (keyVersion "0.2420"))

(branch "dummy ID"
(rule "imp_right" (formula "1") (userinteraction "y"))
(builtin "Update Simplification" (formula "1"))
(builtin "Update Simplification" (formula "2"))
(rule "and_left" (formula "1") (userinteraction "y"))
(rule "and_left" (formula "1") (userinteraction "y"))
(rule "and_left" (formula "1") (userinteraction "y"))
(rule "and_left" (formula "1") (userinteraction "y"))
(rule "all_right" (formula "6") (inst "sk=pc_0") (userinteraction "y"))
(rule "imp_right" (formula "6") (userinteraction "y"))
(rule "and_right" (formula "7") (userinteraction "y"))
(branch " Case 1"
   (rule "commute_eq" (formula "7") (term "0,1") (userinteraction "n"))
   (rule "apply_eq" (formula "7") (term "1,1") (ifseqformula "6") (userinteraction "n"))
   (rule "polySimp_addComm0" (formula "7") (term "0,1,1") (userinteraction "n"))
   (rule "ifthenelse_split" (formula "7") (term "1") (userinteraction "n"))
   (branch " self = pc_0 TRUE"
      (rule "del_cast_1" (formula "8") (term "1") (userinteraction "n"))
      (rule "apply_eq" (formula "8") (term "0,1,1") (ifseqformula "1") (userinteraction "n"))
      (rule "all_left_hide" (formula "3") (inst "t=pc_0") (userinteraction "y"))
      (rule "apply_eq" (formula "8") (term "1,1") (ifseqformula "3") (userinteraction "y"))
      (rule "all_left_hide" (formula "6") (inst "t=pc_0") (userinteraction "y"))
      (rule "imp_left" (formula "6") (userinteraction "y"))
      (branch " Case 1"
         (rule "close_goal" (formula "7") (ifseqformula "2") (userinteraction "y"))
      )
      (branch " Case 2"
         (rule "and_left" (formula "6") (userinteraction "y"))
         (rule "del_cast_1" (formula "8") (term "0") (userinteraction "y"))
         (builtin "Decision procedure Yices")
      )
   )
   (branch " self = pc_0 FALSE"
      (rule "all_left_hide" (formula "5") (inst "t=pc_0") (userinteraction "y"))
      (rule "imp_left" (formula "5") (userinteraction "y"))
      (branch " Case 1"
         (rule "close_goal" (formula "6") (ifseqformula "1") (userinteraction "y"))
      )
      (branch " Case 2"
         (rule "and_left" (formula "5") (userinteraction "y"))
         (rule "close_goal" (formula "9") (ifseqformula "5") (userinteraction "y"))
      )
   )
)
(branch " Case 2"
   (rule "commute_eq" (formula "7") (term "0,0") (userinteraction "n"))
   (rule "apply_eq" (formula "7") (term "1,0") (ifseqformula "6") (userinteraction "n"))
   (rule "polySimp_addComm0" (formula "7") (term "0,1,0") (userinteraction "n"))
   (rule "ifthenelse_split" (formula "7") (term "0") (userinteraction "n"))
   (branch " self = pc_0 TRUE"
      (rule "del_cast_1" (formula "8") (term "0") (userinteraction "n"))
      (rule "apply_eq_rigid" (formula "8") (term "0,1,0") (ifseqformula "1") (userinteraction "n"))
      (rule "all_left_hide" (formula "3") (inst "t=pc_0") (userinteraction "y"))
      (rule "apply_eq" (formula "8") (term "1,0") (ifseqformula "3") (userinteraction "y"))
      (builtin "Decision procedure Yices")
   )
   (branch " self = pc_0 FALSE"
      (builtin "Decision procedure Yices")
   )
)
)

}