Version française
Home     About     Download     Resources     Contact us    
Browse thread
Attach an invariant to a type
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Dawid Toton <d0@w...>
Subject: Attach an invariant to a type
What should I do if I have need for the following? Does already exist 
any equivalent solution?

I'd like to write:

type subindex = int invariant x -> (x>=10)&&(x<=100)

let doit (a:subindex) (b:subindex) =
  let result = some_operation a b in
  (result:subindex)

And it should be translated to:

type subindex = int
let subindex_invariant x = (x>=10)&&(x<=100)

let doit (a:subindex) (b:subindex) =
  assert (subindex_invariant a);
  assert (subindex_invariant b);
  let result = some_operation a b in
  assert (subindex_invariant result);
  (result:subindex)

Am I going right direction at all?

----------------------------------------------------
Promocyjne oferty biletów lotniczych!
Praga, Rzym, Pary¿, Mediolan ju¿ od 499z³ - Kliknij:
http://klik.wp.pl/?adr=http%3A%2F%2Fsamoloty.wp.pl%2Fpromocje%2F&sid=202