ExecutionLog | `- Expected Cost | +- [f] | 0 | +- [Program] | 0:If(minPrice 0) Then | Skip | Else | Abort | 1:While(sPrice 1 + minPrice) | Choice | 1/4: sPrice :~ {1 : 1 + sPrice} | 3/4: sPrice :~ {1 : -1 + sPrice} | numShares :~ {1/4 : 0;1/4 : 1;1/4 : 2;1/4 : 3} | 2:While(numShares 1) | numShares :~ {1 : -1 + numShares} | z :~ {1 : sPrice + z} | Tick(z) | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | 1:While(sPrice 1 + minPrice) | | Choice | | 1/4: sPrice :~ {1 : 1 + sPrice} | | 3/4: sPrice :~ {1 : -1 + sPrice} | | numShares :~ {1/4 : 0;1/4 : 1;1/4 : 2;1/4 : 3} | | 2:While(numShares 1) | | numShares :~ {1 : -1 + numShares} | | z :~ {1 : sPrice + z} | | | `- 0 | +- Expected Cost | | | +- [f] | | 0 | | | +- [Program] | | Tick(z) | | | `- [z | z 0] | +- Expected Cost | | | +- [f] | | [z | z 0] | | | +- [Program] | | 1:While(sPrice 1 + minPrice) | | Choice | | 1/4: sPrice :~ {1 : 1 + sPrice} | | 3/4: sPrice :~ {1 : -1 + sPrice} | | numShares :~ {1/4 : 0;1/4 : 1;1/4 : 2;1/4 : 3} | | 2:While(numShares 1) | | numShares :~ {1 : -1 + numShares} | | z :~ {1 : sPrice + z} | | | +- While.step | | | | | +- [Problem] | | | 1:While(sPrice 1 + minPrice) | | | Choice | | | 1/4: sPrice :~ {1 : 1 + sPrice} | | | 3/4: sPrice :~ {1 : -1 + sPrice} | | | numShares :~ {1/4 : 0;1/4 : 1;1/4 : 2;1/4 : 3} | | | 2:While(numShares 1) | | | numShares :~ {1 : -1 + numShares} | | | z :~ {1 : sPrice + z} | | | | | +- [f] | | | [z | z 0] | | | | | +- While.step | | | | | | | +- [Problem] | | | | 2:While(numShares 1) | | | | numShares :~ {1 : -1 + numShares} | | | | z :~ {1 : sPrice + z} | | | | | | | +- [f] | | | | [z | z 0] | | | | | | | +- linear-template | | | | | | | | | `- 1 + [numShares | numShares 0] + [numShares | numShares 0][sPrice | sPrice 0] + [z | z 0] | | | | | | | +- [Norms] | | | | [[1 | ],[numShares | numShares 0],[numSharessPrice | numShares 0 sPrice 0],[z | z 0]] | | | | | | | +- [Invariant] | | | | numShares 1 ==> 0 + h([1 | ],[-1 + numShares | -1 + numShares 0],[numSharessPrice + -sPrice | -1 + numShares 0 sPrice 0],[sPrice + z | sPrice + z 0]) h([1 | ],[numShares | numShares 0],[numSharessPrice | numShares 0 sPrice 0],[z | z 0]) | | | | 1 1 + numShares ==> [z | z 0] h([1 | ],[numShares | numShares 0],[numSharessPrice | numShares 0 sPrice 0],[z | z 0]) | | | | | | | `- [numSharessPrice | numShares 0 sPrice 0] + [z | z 0] | | | | | +- mixed-lin-template | | | | | | | `- 1 + [1 + sPrice | 1 + sPrice 0][-minPrice + sPrice | -minPrice + sPrice 0] + [1 + sPrice | 1 + sPrice 0][-minPrice + sPrice | -minPrice + sPrice 0]^2 + 2([-minPrice + sPrice | -minPrice + sPrice 0]) + [-minPrice + sPrice | -minPrice + sPrice 0][z | z 0] + [-minPrice + sPrice | -minPrice + sPrice 0]^2 + [z | z 0] | | | | | +- [Norms] | | | [[1 | ],[-minPrice + -minPricesPrice + sPrice + sPrice^2 | 1 + sPrice 0 -minPrice + sPrice 0],[-2(minPricesPrice) + -2(minPricesPrice^2) + minPrice^2 + minPrice^2sPrice + sPrice^2 + sPrice^3 | 1 + sPrice 0 -minPrice + sPrice 0],[-minPrice + sPrice | -minPrice + sPrice 0],[-minPricez + sPricez | -minPrice + sPrice 0 z 0],[-2(minPricesPrice) + minPrice^2 + sPrice^2 | -minPrice + sPrice 0],[z | z 0]] | | | | | +- While.step | | | | | | | +- [Problem] | | | | 2:While(numShares 1) | | | | numShares :~ {1 : -1 + numShares} | | | | z :~ {1 : sPrice + z} | | | | | | | +- [f] | | | | [-minPricez + sPricez | -minPrice + sPrice 0 z 0] | | | | | | | +- linear-template | | | | | | | | | `- 1 + [-minPricez + sPricez | -minPrice + sPrice 0 z 0] + [-minPricesPrice + sPrice^2 | -minPricesPrice + sPrice^2 0][numShares | numShares 0] + [numShares | numShares 0] | | | | | | | +- [Norms] | | | | [[1 | ],[-minPricez + sPricez | -minPrice + sPrice 0 z 0],[-minPricenumSharessPrice + numSharessPrice^2 | -minPricesPrice + sPrice^2 0 numShares 0],[numShares | numShares 0]] | | | | | | | +- [Invariant] | | | | numShares 1 ==> 0 + h([1 | ],[-minPricesPrice + -minPricez + sPricez + sPrice^2 | -minPrice + sPrice 0 sPrice + z 0],[-minPricenumSharessPrice + minPricesPrice + numSharessPrice^2 + -sPrice^2 | -1 + numShares 0 -minPricesPrice + sPrice^2 0],[-1 + numShares | -1 + numShares 0]) h([1 | ],[-minPricez + sPricez | -minPrice + sPrice 0 z 0],[-minPricenumSharessPrice + numSharessPrice^2 | -minPricesPrice + sPrice^2 0 numShares 0],[numShares | numShares 0]) | | | | 1 1 + numShares ==> [-minPricez + sPricez | -minPrice + sPrice 0 z 0] h([1 | ],[-minPricez + sPricez | -minPrice + sPrice 0 z 0],[-minPricenumSharessPrice + numSharessPrice^2 | -minPricesPrice + sPrice^2 0 numShares 0],[numShares | numShares 0]) | | | | | | | `- [-minPricez + sPricez | -minPrice + sPrice 0 z 0] + [-minPricenumSharessPrice + numSharessPrice^2 | -minPricesPrice + sPrice^2 0 numShares 0] | | | | | +- [Invariant] | | | sPrice 1 + minPrice ==> 0 + h([1 | ],1/4[2 + -2(minPrice) + -minPricesPrice + 3(sPrice) + sPrice^2 | 1 + -minPrice + sPrice 0 2 + sPrice 0] + 3/4[-minPricesPrice + -sPrice + sPrice^2 | -1 + -minPrice + sPrice 0 sPrice 0],1/4[2 + -4(minPrice) + -6(minPricesPrice) + -2(minPricesPrice^2) + 2(minPrice^2) + minPrice^2sPrice + 5(sPrice) + 4(sPrice^2) + sPrice^3 | 1 + -minPrice + sPrice 0 2 + sPrice 0] + 3/4[2(minPricesPrice) + -2(minPricesPrice^2) + minPrice^2sPrice + sPrice + -2(sPrice^2) + sPrice^3 | -1 + -minPrice + sPrice 0 sPrice 0],1/4[1 + -minPrice + sPrice | 1 + -minPrice + sPrice 0] + 3/4[-1 + -minPrice + sPrice | -1 + -minPrice + sPrice 0],1/16[-minPricez + sPricez + z | 1 + -minPrice + sPrice 0 z 0] + 1/16[-minPricez + sPricez + z | 1 + -minPrice + sPrice 0 z 0] + 1/16[1 + -minPrice + -minPricesPrice + 2(sPrice) + sPrice^2 | 1 + -minPrice + -minPricesPrice + 2(sPrice) + sPrice^2 0] + 1/16[-minPricez + sPricez + z | 1 + -minPrice + sPrice 0 z 0] + 1/8[1 + -minPrice + -minPricesPrice + 2(sPrice) + sPrice^2 | 1 + -minPrice + -minPricesPrice + 2(sPrice) + sPrice^2 0] + 1/16[-minPricez + sPricez + z | 1 + -minPrice + sPrice 0 z 0] + 3/16[1 + -minPrice + -minPricesPrice + 2(sPrice) + sPrice^2 | 1 + -minPrice + -minPricesPrice + 2(sPrice) + sPrice^2 0] + 3/16[-minPricez + sPricez + -z | -1 + -minPrice + sPrice 0 z 0] + 3/16[-minPricez + sPricez + -z | -1 + -minPrice + sPrice 0 z 0] + 3/16[1 + minPrice + -minPricesPrice + -2(sPrice) + sPrice^2 | 1 + minPrice + -minPricesPrice + -2(sPrice) + sPrice^2 0] + 3/16[-minPricez + sPricez + -z | -1 + -minPrice + sPrice 0 z 0] + 3/8[1 + minPrice + -minPricesPrice + -2(sPrice) + sPrice^2 | 1 + minPrice + -minPricesPrice + -2(sPrice) + sPrice^2 0] + 3/16[-minPricez + sPricez + -z | -1 + -minPrice + sPrice 0 z 0] + 9/16[1 + minPrice + -minPricesPrice + -2(sPrice) + sPrice^2 | 1 + minPrice + -minPricesPrice + -2(sPrice) + sPrice^2 0],1/4[1 + -2(minPrice) + -2(minPricesPrice) + minPrice^2 + 2(sPrice) + sPrice^2 | 1 + -minPrice + sPrice 0] + 3/4[1 + 2(minPrice) + -2(minPricesPrice) + minPrice^2 + -2(sPrice) + sPrice^2 | -1 + -minPrice + sPrice 0],1/16[z | z 0] + 1/16[1 + sPrice | 1 + sPrice 0] + 1/16[z | z 0] + 1/8[1 + sPrice | 1 + sPrice 0] + 1/16[z | z 0] + 3/16[1 + sPrice | 1 + sPrice 0] + 1/16[z | z 0] + 3/16[z | z 0] + 3/16[-1 + sPrice | -1 + sPrice 0] + 3/16[z | z 0] + 3/8[-1 + sPrice | -1 + sPrice 0] + 3/16[z | z 0] + 9/16[-1 + sPrice | -1 + sPrice 0] + 3/16[z | z 0]) h([1 | ],[-minPrice + -minPricesPrice + sPrice + sPrice^2 | 1 + sPrice 0 -minPrice + sPrice 0],[-2(minPricesPrice) + -2(minPricesPrice^2) + minPrice^2 + minPrice^2sPrice + sPrice^2 + sPrice^3 | 1 + sPrice 0 -minPrice + sPrice 0],[-minPrice + sPrice | -minPrice + sPrice 0],[-minPricez + sPricez | -minPrice + sPrice 0 z 0],[-2(minPricesPrice) + minPrice^2 + sPrice^2 | -minPrice + sPrice 0],[z | z 0]) | | | 1 + minPrice 1 + sPrice ==> [z | z 0] h([1 | ],[-minPrice + -minPricesPrice + sPrice + sPrice^2 | 1 + sPrice 0 -minPrice + sPrice 0],[-2(minPricesPrice) + -2(minPricesPrice^2) + minPrice^2 + minPrice^2sPrice + sPrice^2 + sPrice^3 | 1 + sPrice 0 -minPrice + sPrice 0],[-minPrice + sPrice | -minPrice + sPrice 0],[-minPricez + sPricez | -minPrice + sPrice 0 z 0],[-2(minPricesPrice) + minPrice^2 + sPrice^2 | -minPrice + sPrice 0],[z | z 0]) | | | | | `- 3[-minPrice + -minPricesPrice + sPrice + sPrice^2 | 1 + sPrice 0 -minPrice + sPrice 0] + 3[-minPrice + sPrice | -minPrice + sPrice 0] + 3/4[-2(minPricesPrice) + minPrice^2 + sPrice^2 | -minPrice + sPrice 0] + [z | z 0] | | | `- 3[-minPrice + -minPricesPrice + sPrice + sPrice^2 | 1 + sPrice 0 -minPrice + sPrice 0] + 3[-minPrice + sPrice | -minPrice + sPrice 0] + 3/4[-2(minPricesPrice) + minPrice^2 + sPrice^2 | -minPrice + sPrice 0] + [z | z 0] | `- [minPrice 0] (3[-minPrice + -minPricesPrice + sPrice + sPrice^2 | 1 + sPrice 0 -minPrice + sPrice 0] + 3[-minPrice + sPrice | -minPrice + sPrice 0] + 3/4[-2(minPricesPrice) + minPrice^2 + sPrice^2 | -minPrice + sPrice 0] + [z | z 0]) [Success] [minPrice 0] (3[-minPrice + -minPricesPrice + sPrice + sPrice^2 | 1 + sPrice 0 -minPrice + sPrice 0] + 3[-minPrice + sPrice | -minPrice + sPrice 0] + 3/4[-2(minPricesPrice) + minPrice^2 + sPrice^2 | -minPrice + sPrice 0] + [z | z 0]) Degree: 2