File: loop0.mlw

package info (click to toggle)
why 2.26%2Bdfsg-2%2Bsqueeze1
  • links: PTS, VCS
  • area: main
  • in suites: squeeze
  • size: 19,796 kB
  • ctags: 19,175
  • sloc: ml: 115,078; java: 9,253; ansic: 4,757; makefile: 1,350; sh: 485; lisp: 3
file content (18 lines) | stat: -rw-r--r-- 353 bytes parent folder | download | duplicates (4) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
 

(* Simple loop. 
 
   Decreases reference [x] down to [0].
   While not necessary to establish postcondition [x = 0] we add
   [x <= x@0] to the invariant to illustrate the use of labels. *)

parameter x : int ref

let p () = 
  { x >= 0 }
  init:
  while !x > 0 do 
    { invariant 0 <= x <= x@init  variant x } 
    x := !x - 1 
  done 
  { x = 0 }