test-claude.mlw 900 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2


MARCHE Claude's avatar
MARCHE Claude committed
3 4
module TestBool

5
  use bool.Bool
MARCHE Claude's avatar
MARCHE Claude committed
6 7 8 9 10 11 12 13 14

  let f (x:bool) : bool
  ensures { result = True }
  =
    if x then False else x

end


MARCHE Claude's avatar
MARCHE Claude committed
15 16
module M

17 18
  use int.Int
  use ref.Ref
MARCHE Claude's avatar
MARCHE Claude committed
19

20 21
  val f (n:int) : bool
    ensures { if result then n >= 0 else n <= 0 }
22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38
end


module Termination


  type t = A t | B

  predicate p (x:t) =
    match x with
    | A y -> p y
    | B -> true
    end

  predicate q (x:t) =
    match x with
    | A (A y) -> q y
39
    | A _y -> false
40 41 42 43 44 45 46 47 48 49 50 51 52
    | B -> true
    end

  type t1 = E t2
  with t2 = C t1 | D

  predicate r (x:t1) =
    match x with
    | E (C y) -> r y
    | E D -> true
    end


53 54 55 56 57 58 59
  let rec f "W:diverges:N" (x:t) : t =
    let _y = 42 in
    f x

  let g "W:diverges:N" (x:t) : t =
    while true do () done; x

MARCHE Claude's avatar
MARCHE Claude committed
60 61 62 63 64
end


module Absurd

65
use int.Int
MARCHE Claude's avatar
MARCHE Claude committed
66 67 68 69 70 71

let f (x:int) : int =
  if x = 0 then 0 else
  if x > 0 then (assert {1=1} ; 1) else
  if x < 0 then -1 else(assert {1=1}; absurd)

MARCHE Claude's avatar
MARCHE Claude committed
72
end