English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

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: 2008-01-31 (13:29)
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

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);

Am I going right direction at all?

Promocyjne oferty biletów lotniczych!
Praga, Rzym, Pary¿, Mediolan ju¿ od 499z³ - Kliknij: