http://d.puremagic.com/issues/show_bug.cgi?id=7584
--- Comment #10 from timon.g...@gmx.ch 2012-05-03 08:53:53 PDT --- (In reply to comment #9) > (In reply to comment #0) > > IIRC, this is how contract inheritance works in Spec#. Spec# is (ahead of) > > state of the art in this area. > > According to my reading of > http://http://research.microsoft.com/en-us/um/people/leino/papers/krml136.pdf, > page 9, paragraph 1, Spec# does not allow overriding of preconditions so it > can't be used here as an example. This seems to be correct. Thank you for looking it up. -- Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email ------- You are receiving this mail because: -------