Il y a huit mots dans cette phrase, Il n'y a pas huit mots dans cette phrase

MACHINE
phrasesParadoxales
/* Le contraire d'une vérité n'est pas toujours un mensonge :
"Il y a huit mots dans cette phrase". Vrai.
"Il n'y a pas huit mots dans cette phrase" Vrai aussi !
La traduction de ce texte en anglais constitue cette fois deux
mensonges au lieu de deux vérités :
There is eight words in this sentence. Faux.
There is not eight words in this sentence. Faux aussi !*/
SETS
MOT ={il, y, a, huit, mots, dans, cette, phrase,n', pas}
CONSTANTS
phrase1, phrase2
PROPERTIES
phrase1 : seq(MOT) & phrase2 : seq(MOT) &
phrase1 =[il, y, a , huit, mots, dans, cette, phrase] &
phrase2 = [il, n', y, a, pas, huit, mots, dans, cette, phrase]
bool(card(dom(phrase1))=8) = TRUE &
bool(card(dom(phrase2))=8) = FALSE &

bool(not(card(dom(phrase1))=8)) = TRUE


END

/* Cette machine ne passe pas la phase de Type Check sur l'Atelier B car il y a des identificateurs qui ont moins de 2 caractères */

/*La spéc suivante passe la phase de type check. Mais quand on lance la génération des OP, on
obtient le message suivant : STRING type can only be used to type operations input parameters,
with the belong predicate */
Nota : ne mettez pas d'accents dans les commentaires d'une spéc que vous voulez conduire jusqu'au code ADA, voir les conseils sur un précédent message.

MACHINE
phrasesParadoxales
/* Le contraire d'une vérité n'est pas toujours un mensonge :
"Il y a huit mots dans cette phrase". Vrai.
"Il n'y a pas huit mots dans cette phrase" Vrai aussi !
La traduction de ce texte en anglais constitue cette fois deux
mensonges au lieu de deux vérités :
There is eight words in this sentence. Faux.
There is not eight words in this sentence. Faux aussi !*/

CONSTANTS
phrase1, phrase2, mots
PROPERTIES
mots <: STRING & mots = {"il"," y", "a", "huit", "mots", "dans", "cette", "phrase","n'", "pas"}
phrase1 : seq(mots) & phrase2 : seq(mots) &
phrase1 =["il"," y", "a", "huit", "mots", "dans", "cette", "phrase"] &
phrase2 = ["il", "n'"" y", "a", "pas", "huit", "mots", "dans", "cette", "phrase"]
bool(card(dom(phrase1))=8) = TRUE &
bool(card(dom(phrase2))=8) = FALSE &

bool(not(card(dom(phrase1))=8)) = TRUE


END