The Atelier Focal

Show Task #

Task #181 Preuve Zenon non explicable

Opened by Philippe Ayrault (phil) - 15 Nov 2008
Last edited by François Pessaux (francois) - 10 Jun 2009

Task Type	Bug Report
Category	Zenon
Status	Assigned
Assigned To	Damien Doligez (doligez)
Operating System	All

Severity	Medium
Reported Version	Current
Due in Version	Undecided
Percent Complete

Details

J'ai un soucis, il me semble que j'arrive Ã prouver une propriÃ©tÃ© avec Zenon alors que je n'ai pas fourni de preuve. Je joins un programme avec 2 variantes et les 2 traces de compilation.
Philippe

Compilation de la premiere version:
focalize -I /home/phil/Tools/FoCal/focal/focalize/stdlib -I /home/phil/Tools/FoCal/focal/focalize/extlib/algebra -I /home/phil/Lip6/These/FoCal/Utils_focalize pb.foc
zvtov -new -zenon /home/phil/Tools/FoCal/focal/zenon/zenon -zz -max-time -zz 3m pb.zv
File "pb.foc", line 16, characters 0-38:
Warning: defined symbol basics.syntactic_equal is used with wrong arity
### proof failed
File "pb.foc", line 12, characters 0-12:
### proof failed
File "pb.foc", line 20, characters 0-13:
### proof failed

Il y a un warning que je ne comprends pas.
et les 3 propriÃ©tÃ©s ne sont pas prouvÃ©es.

Compilation de la seconde version (inversion des lignes en commentaire)
focalize -I /home/phil/Tools/FoCal/focal/focalize/stdlib -I /home/phil/Tools/FoCal/focal/focalize/extlib/algebra -I /home/phil/Lip6/These/FoCal/Utils_focalize pb.foc
zvtov -new -zenon /home/phil/Tools/FoCal/focal/zenon/zenon -zz -max-time -zz 3m pb.zv
File "pb.foc", line 16, characters 0-38:
### proof failed
File "pb.foc", line 12, characters 0-12:
### proof failed

Le message d'erreur a disparu, et la troisiÃ¨me propritÃ© a Ã©tÃ© prouvÃ© alors que je n'ai fourni aucune preuve mais 2 fois la mÃªme preuve prÃ©cÃ©demment fausse de la mÃªme propriÃ©tÃ© (diff_green_blue) !!

Question subsidiaire ; comment faire ses preuves en Zenon ?

Le programme :
use "basics";;

open "basics";;

species Requests inherits Basic_object =
signature blue : Self;
signature red : Self;
signature green : Self;

property diff_blue_red :
~ blue = red
;

property diff_green_blue :
~ basics#syntactic_equal( green, blue)
;

property diff_green_red :
~ green = red
;

end;;

species Imp_request inherits Requests =
rep = int;

let blue = 1;
let red = 2;
let green = 3;

proof of diff_blue_red =
by definition of basics#syntactic_equal
;

proof of diff_green_blue =
by definition of basics#syntactic_equal
;

(* Ligne Ã inverser
proof of diff_green_blue =
*)
proof of diff_green_red =
by
;

end;;

Comment by François Pessaux - Friday, 21 Nov 2008, 10:19am

Bon,en fait il y a beaucoup de choses Ã dire dans tout Ã§a:

1) "et la troisiÃ¨me propritÃ© a Ã©tÃ© prouvÃ© alors que je n'ai fourni aucune preuve mais 2 fois la mÃªme preuve prÃ©cÃ©demment fausse de la mÃªme propriÃ©tÃ©"

Non, la 3Ã¨me propriÃ©tÃ© n'a PAS Ã©tÃ© prouvÃ©e puisque tu l'as supprimÃ©e ! Ta preuve de 'diff_green_red' n'existe PLUS. Donc elle n'est pas rÃ©solue par Zenon.

2) Le seul bug que l'on peu reprocher au compilo c'est qu'il ne t'ai pas rÃ¢lÃ© dessus car tu as donnÃ© dans la mÃªme espÃ¨ce 2 preuves d'une mÃªme propriÃ©tÃ©.

3) L'histoire de "Warning: defined symbol basics.syntactic_equal...", lÃ par contre, je pense que c'est Damien qui serait le mieux placer pour en parler.

Comment by François Pessaux - Friday, 21 Nov 2008, 11:39am
Donc, un message d'erreur est dÃ©sormais rajoutÃ© lorsque l'on trouve plusieurs "proof of" d'une mÃªme propriÃ©tÃ© dans une espÃ¨ce (dans sno corps, pas par hÃ©ritage bien sÃ»r).

Comment by Damien Doligez - Tuesday, 23 Dec 2008, 2:39pm
Le warning a disparu, j'ai du le corriger a un moment donne. Pour la question subsidiaire, il faut attendre que Zenon fasse l'arithmetique, et c'est pas gagne...