http://d.puremagic.com/issues/show_bug.cgi?id=7584



--- Comment #10 from timon.gehr@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: -------