Am 19.04.2010 20:26, schrieb Jamey Sharp: > Yes, I used to know someone who used Promela/Spin, and that would be awesome. > > We actually have proofs or proof sketches for parts of XCB, so for > example I am Confident that pure XCB applications will never fail to > insert GetInputFocus requests when needed to maintain sequence number > synchronization, and also that it will always do so at the last > possible instant. (I can also prove by counterexample that Xlib > doesn't have either of these properties :-/ which would require huge > ABI changes to fix.) We haven't used model-checkers for that, just > logic and Hoare triples or Z. Nice! Is that published/documented somewhere?
-- Simon _______________________________________________ [email protected]: X.Org development Archives: http://lists.x.org/archives/xorg-devel Info: http://lists.x.org/mailman/listinfo/xorg-devel
