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.
|ID0001978||Frama-Clang||Plug-in > clang||public||2014-11-20||2015-02-16|
|Product Version||-||Target Version||-||Fixed in Version||-|
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.