[Issue 7584] contract checking is too conservative for inherited contracts

[d-bugmail at puremagic.com]

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


Andrei Alexandrescu <andrei at metalanguage.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |andrei at metalanguage.com


--- Comment #9 from Andrei Alexandrescu <andrei at metalanguage.com> 2012-05-03 07:44:53 PDT ---
(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.

-- 
Configure issuemail: http://d.puremagic.com/issues/userprefs.cgi?tab=email
------- You are receiving this mail because: -------