Liskov substitution principle not checked for methods of same name and signature in super- and subclass
ID0001978: This issue was created automatically from Mantis Issue 1978. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001978 | Frama-Clang | Plug-in > clang | public | 2014-11-20 | 2015-02-16 |
| Reporter | Jochen | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | frama-c-Neon-20140301+dev-stance | OS | - | OS Version | xubuntu-cfe13.10 |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
This is not a bug report but merely a suggestion for discussion. According to the "Liskov substitution principle" (see the English wikipedia article of that name for references) a method in a subclass should have a stronger (or equivalent) contract that the corresponding method in the superclass. It could make sense to provide a corresponding check within Frama-Cxx, which could be enabled or disabled by an appropriate command-line option.
This check would be negative (i.e. unprovable) for the attached program "140.cpp"; however, it would be positive if "==" in line 3 was changed to ">=". So this program can be used as a simple test case for such a check, if and when it is implemented.