Verification of programs using inspector methods

摘要: Most classes in an object-oriented program provide access to object’s state through methods, so that client code does not depend on and cannot interfere with the internal representation composed of fields component objects. Methods used for this purpose are sometimes called inspector methods. In order extend benefits methods specifications, method contracts non-inspector may be expressed using hence providing support abstraction specifications. paper, we propose approach verification programs use object invariants. Inspector have parameters, they objects passed as arguments. Our builds Boogie methodology invariants ownership. Performing a programming language allows aliasing references poses framing problem. Specifically, needs able tell whether modifying given or calling affect value call. We solve by modeling functions take arguments only those parts heap which depend. Thanks novel logical encoding heap, can do without breaking information hiding, even cases where The core our has been implemented custom build Spec# verifier.