ExecutionLog | `- Expected Cost | +- [f] | 0 | +- [Program] | 0:If(y 0) Then | Skip | Else | Abort | 1:While(x 1) | x :~ {1 : -1 + x} | Choice | 1/4: y :~ {1 : 1 + y} | 3/4: Skip | 2:While(y 1) | y :~ {1 : -1 + y} | Tick(1) | Tick(2) | +- While.step | | | +- [Problem] | | 1:While(x 1) | | x :~ {1 : -1 + x} | | Choice | | 1/4: y :~ {1 : 1 + y} | | 3/4: Skip | | 2:While(y 1) | | y :~ {1 : -1 + y} | | Tick(1) | | Tick(2) | | | +- [f] | | 0 | | | +- Expected Cost Body | | | | | +- Expected Cost | | | | | | | +- [f] | | | | 0 | | | | | | | +- [Program] | | | | 2:While(y 1) | | | | y :~ {1 : -1 + y} | | | | Tick(1) | | | | | | | +- While.step | | | | | | | | | +- [Problem] | | | | | 2:While(y 1) | | | | | y :~ {1 : -1 + y} | | | | | Tick(1) | | | | | | | | | +- [f] | | | | | 0 | | | | | | | | | +- Expected Cost Body | | | | | | | | | | | `- [1 | ] | | | | | | | | | +- linear-template | | | | | | | | | | | `- 1 + [y | y 0] | | | | | | | | | +- [Norms] | | | | | [[1 | ],[y | y 0]] | | | | | | | | | +- [Invariant] | | | | | y 1 ==> [1 | ] + h([1 | ],[-1 + y | -1 + y 0]) h([1 | ],[y | y 0]) | | | | | 1 1 + y ==> 0 h([1 | ],[y | y 0]) | | | | | | | | | `- [y | y 0] | | | | | | | `- [y | y 0] | | | | | +- Expected Cost | | | | | | | +- [f] | | | | 0 | | | | | | | +- [Program] | | | | Tick(2) | | | | | | | `- 2 | | | | | +- Expected Cost | | | | | | | +- [f] | | | | 2 | | | | | | | +- [Program] | | | | 2:While(y 1) | | | | y :~ {1 : -1 + y} | | | | Tick(1) | | | | | | | `- 2 | | | | | `- 1/4[1 + y | 1 + y 0] + 1/2 + 3/4[y | y 0] + 3/2 | | | +- linear-template | | | | | `- 1 + [1 + y | 1 + y 0] + [x | x 0] + [y | y 0] | | | +- [Norms] | | [[1 | ],[1 + y | 1 + y 0],[x | x 0],[y | y 0]] | | | +- While.step | | | | | +- [Problem] | | | 2:While(y 1) | | | y :~ {1 : -1 + y} | | | Tick(1) | | | | | +- [f] | | | [1 + y | 1 + y 0] | | | | | +- linear-template | | | | | | | `- 1 + [1 + y | 1 + y 0] + 2([y | y 0]) | | | | | +- [Norms] | | | [[1 | ],[1 + y | 1 + y 0],[y | y 0]] | | | | | +- [Invariant] | | | y 1 ==> 0 + h([1 | ],[y | y 0],[-1 + y | -1 + y 0]) h([1 | ],[1 + y | 1 + y 0],[y | y 0]) | | | 1 1 + y ==> [1 + y | 1 + y 0] h([1 | ],[1 + y | 1 + y 0],[y | y 0]) | | | | | `- [1 | ] | | | +- While.step | | | | | +- [Problem] | | | 2:While(y 1) | | | y :~ {1 : -1 + y} | | | Tick(1) | | | | | +- [f] | | | [y | y 0] | | | | | +- linear-template | | | | | | | `- 1 + 3([y | y 0]) | | | | | +- [Norms] | | | [[1 | ],[y | y 0]] | | | | | +- [Invariant] | | | y 1 ==> 0 + h([1 | ],[-1 + y | -1 + y 0]) h([1 | ],[y | y 0]) | | | 1 1 + y ==> [y | y 0] h([1 | ],[y | y 0]) | | | | | `- 0 | | | +- [Invariant] | | x 1 ==> 1/4[1 + y | 1 + y 0] + 1/2 + 3/4[y | y 0] + 3/2 + h([1 | ],[1 | ],[-1 + x | -1 + x 0],0) h([1 | ],[1 + y | 1 + y 0],[x | x 0],[y | y 0]) | | 1 1 + x ==> 0 h([1 | ],[1 + y | 1 + y 0],[x | x 0],[y | y 0]) | | | `- 9/4[x | x 0] + [y | y 0] | `- [y 0] (9/4[x | x 0] + [y | y 0]) [Success] [y 0] (9/4[x | x 0] + [y | y 0]) Degree: 1