File: exceptions.mlw

package info (click to toggle)
why3 1.8.2-3
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid
  • size: 45,028 kB
  • sloc: xml: 185,443; ml: 111,224; ansic: 3,998; sh: 2,578; makefile: 2,568; java: 865; python: 720; javascript: 290; lisp: 205; pascal: 173
file content (22 lines) | stat: -rw-r--r-- 294 bytes parent folder | download | duplicates (5) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
 
module M

use int.Int
use ref.Ref

exception Break

let f (n : int) : int ensures { result <= 10 }
= let i = ref n in
  try
    while (!i > 0) do
      invariant { true }
      variant { !i }
      if (!i <= 10) then raise Break;
      i := !i - 1
    done
  with Break -> ()
  end;
  !i

end