The Strong Object Invariant
Journal Title: TEM JOURNAL - Year 2012, Vol 1, Issue 1
Abstract
The concept of an invariant is fundamental to object-oriented programming, because it provides information on the overall behaviour of the class and/or its objects. An invariant is a predicate, that is true in every state that is proclaimed as valid. A strong invariant is a predicate, that is true in every valid state and false in every invalid state. Basically, we can divide them into two categories: object invariants and class invariants. Object invariants describe the consistency of object, i.e. non-static fields. Analysis of invariants takes the most important place in object-oriented program verification and can be directed in two ways – as prescribed and as described. This paper considers both analyses which are based on the strongest dynamic postconditions of methods with the guard as the precondition, thus, determining all possible transitions and only them. In addition, since dynamic postconditions are logical functions of the initial-final states, our solution is based solely on the first-order predicate logic.
Authors and Affiliations
Dusan Malbaski, Aleksandar Kupusinac
Keywords
Related Articles
- EP ID EP103258
- DOI -
- Views 182
- Downloads 0
One implementation of API interface for RouterOS
The purpose of this publication is to present the implementation of API interface for RouterOS of the company MikroTik, which allows using PHP scripts for obtaining data for configuration and management of the routing de...
Investigation of Partially Crystalline Zr77Ni23 Metallic Glass
This paper presents the results of an extensive research of partially crystalline Zr77Ni23 metallic glass (indicated numbers refer to atomic percentages). The partially crystalline Zr77Ni23 samples were prepared by...
Modeling of Three Dimensional Magnetic Field in Three-Phase Induction Motor with Double Squirrel Cage
From three-phase induction machines, asynchronous double-cage rotor motors stand out as more specific, as in the construction and after the performance. Such a type of motor is selected as the objective of a study, and i...
A New Perspective: Organizational Citizenship Behaviour and its Reflections
Organizational citizenship behaviour is not only confined to the behaviours of the organizational workers in accordance with the definitions of their roles, but it also includes all the other behaviours they di...
Application for Warehousing and OLAP Analysis of Data about Unique Bulgarian Bells
In this paper, the system bgBell/OLAP for warehousing and online analytical processing data about unique Bulgarian bells is proposed. The implemented system provides possibility for retrieving summar...