File: loop0.mlw

package info (click to toggle)
why 2.30%2Bdfsg-5
  • links: PTS, VCS
  • area: main
  • in suites: wheezy
  • size: 26,916 kB
  • sloc: ml: 116,979; java: 9,376; ansic: 5,175; makefile: 1,335; sh: 531; lisp: 127
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 }