Dear Andrei, I’m also slow because of travelling to Nice...
> Le 28 mai 2019 à 15:27, Andrei Paskevich <andrei.paskev...@lri.fr> a écrit : > > Dear Jean-Jacques, > > very late and very partial answer: > > On Wed, 10 Apr 2019 at 17:38, Jean-Jacques Levy <jean-jacques.l...@inria.fr > <mailto:jean-jacques.l...@inria.fr>> wrote: > 1- ide: stop pop-up menus. No reason for them, or make them optional. It > makes a shaky behaviour. When thinking on a proof, it’s very bad to see > sparkling menus. Furthermore, the macOS X-window handles them strangely when > on border of a window. > > Do you mean contextual menus that appear upon the right mouse click? Or do > you mean error/warning messages that appear in popup windows? I mean contextual menus. It remind me the Xerox Dorado. When thinking of a (difficult) proof, you want a stable screen. X-window on MacOs clip pop-up menus when you are at bottom of screen, enforcing you to reduce the height of the window and acting again the pop-up menu. Maybe x-window on Linux has not same behavior? > 2- ide: stop fancy moves. Jumping to next unproved goal is very confusing, > when you prove goals in non sequential order. Same to jump to a new Emacs > window when choosing Coq as prover. > There is a recenly added option (in the master branch) that makes this > behaviour optional. In the IDE, menu "File", line "Preferences", tab > "General", option "jump to the next unproved goal ». ok so it’s better, but I’m not in favour of jumping to next release, because I want my proofs first be stable. > 3- ide: I loved the display of times on goals. This feature vanished at top > level !! > > It is still there, the third column in the session tree window. However, if > the second column "Theory/Goal" becomes too large, it pushes the third column > "Time" too far right, out of visibility. and with new way of having more interactive proofs + treatment of post-conditions (ie not splitting them on conditional branches) the goals are more pushed to the right. > 7- I still have difficulties with the new treatment of ghost variables. This > end with strange text as the sketchy one which follows: > ------------------------------- > type vertex > let ghost function (!) (s: S.t) = s.contents > val (=) (x y: vertex) : bool ensures { result <-> x = y } > > clone import appmap.Appmap as M with type key = vertex > clone import appset.Appset as S with type elt = vertex > > val constant vertices: S.t > > type env = {ghost black: set vertex; ghost gray: set vertex; > stack: list vertex; sccs: set (set vertex); sn: int; num: M.t int} > > let rec dfs1 x e = > requires {mem x !vertices} > ... > with dfs roots e = > requires {subset !roots !vertices} > returns {(_, e') -> subset !roots (union e'.black e'.gray)} > > if S.is_empty roots then (infty(), e) else > let x = S.choose roots in > let roots' = S.remove x roots in > let (n1, e1) = > if e.num[x] <> -1 then (e.num[x], e) else dfs1 x e in > let (n2, e2) = dfs roots' e1 in (min n1 n2, e2) > ------------------------------ > I thanks Andreij for giving me hints about equality but I dislike my (!), > which could conflict later with references !! Maybe there is smarter way for > distinguishing test-for-emptyness or others in program text ? Maybe another > analysis of ghost variables is feasible ? > > Sorry, I don't understand the example or the question. What do you mean by > "distinguishing test-for-emptyness »? I mean that the program text is uglier. One good point of Hoare logic is that the logic values are nearly same as the program text values. Now for capturing a problem due to the soundness analysis of ghost values, one spoils program text and distinguish between program values and logic values! That’s exactly what I do not like with denotational semantics and now in beautiful Why3, you have similar problems :-( :-( :-( ... > > Best, > Andrei
_______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
