langage

Prédicat pour les preuves / contrats : contient-information.

Exemple :

Contrat pour e = liste->ensemble(l)

∀ x ∈ l, e contient-information x

Cela signifie que e contient suffisamment d'informations pour reproduire x, après, il peut y avoir de la compression, etc. dans la manière de stocker cette information, mais ça nous regarde pas.

Pourrait être utilisée pour des données qu'on envoie sur le réseau : il faut que la donnée soit dans le format de destination, mais on n'a pas besoin de la revoir un jour.

Autre prédicat, plus utile :

contient-information-accessible

Qui signifie qu'on peut récupérer x depuis la structure opaque produite.