# Commits

committed 47deea8 Draft

Edited online

• Participants
• Parent commits 1accb0b

# Home.wiki

` {{{`
` #!boogie`
` `
`-procedure F(n: int) returns (r: int)`
`-  ensures n <= 100 ==> r == 91;`
`-{`
`-  if (100 <= n) {`
`-    r := n - 10;`
`-  } else {`
`-    call r := F(n + 11);`
`-    call r := F(r);`
`-  }`
`-}`
`+1:  procedure F(n: int) returns (r: int)`
`+2:    ensures n <= 100 ==> r == 91;`
`+3:  {`
`+4:    if (100 <= n) {`
`+5:      r := n - 10;`
`+6:    } else {`
`+7:      call r := F(n + 11);`
`+8:      call r := F(r);`
`+9:    }`
`+10: }`
` }}}`
` `
` The Boogie verifier can only [[http://rise4fun.com/Boogie/OItH|tell us]] that the postcondition might not hold.`
` it will produce the following output:`
` `
` {{{`
`-Test cases: 7`
`+Test cases: 8`
` Passed: 0`
` Invalid: 0`
`-Failed: 7 (1 unique)`
`-F(n = -3) failed:  Postcondition "n <= 100 ==> r == 91" defined at McCarthy-91.bpl line 4 violated at McCarthy-91.bpl line 2`
`-                   with n = 100`
`-                        r = 90`
`-                   in call to F at examples/McCarthy-91.bpl line 10`
`-                   ...`
`+Non executable: 0`
`+Failed: 8 (1 unique)`
`+`
`+Failure 0`
`+F(0) failed`
`+`
`+Postcondition "n <= 100 ==> r == 91" defined at McCarthy-91.bpl line 2 violated at McCarthy-91.bpl line 1`
`+with`
`+    n = 100`
`+    r = 90`
`+in call to F at examples/McCarthy-91.bpl line 8`
`+...`
` }}}`
` `
` The failing test case hints us at the problem:`