ExecutionLog
|
`- Expected Cost
   |
   +- [f]
   |    0
   |
   +- [Program]
   |    flag :~ {1 : 1}
   |    i :~ {1 : 0}
   |    0:While(flag  1   k  1 + i)
   |        Choice
   |          1/2: flag :~ {1 : 0}
   |          1/2: flag :~ {1 : 1}
   |        i :~ {1 : 1 + i}
   |        Tick(1)
   |
   +- While.step
   |  |
   |  +- [Problem]
   |  |    0:While(flag  1   k  1 + i)
   |  |        Choice
   |  |          1/2: flag :~ {1 : 0}
   |  |          1/2: flag :~ {1 : 1}
   |  |        i :~ {1 : 1 + i}
   |  |        Tick(1)
   |  |
   |  +- [f]
   |  |    0
   |  |
   |  +- Expected Cost Body
   |  |  |
   |  |  `- [1 | ]
   |  |
   |  +- linear-template
   |  |  |
   |  |  `- 1 + [flag | flag  0] + [-i + k | -i + k  0]
   |  |
   |  +- [Norms]
   |  |    [[1 | ],[flag | flag  0],[-i + k | -i + k  0]]
   |  |
   |  +- [Invariant]
   |  |    flag  1   k  1 + i ==> [1 | ] + h([1 | ],1/2,[-1 + -i + k | -1 + -i + k  0])  h([1 | ],[flag | flag  0],[-i + k | -i + k  0])
   |  |    1  1 + flag   1 + i  1 + k ==> 0  h([1 | ],[flag | flag  0],[-i + k | -i + k  0])
   |  |
   |  `- [-i + k | -i + k  0]
   |
   `- [k | k  0]

[Success] [k | k  0]
Degree: 1