Geodesic
Separable object-oriented program verification with C++ class protocol definition in terms of Petri nets
Modelirovanie i analiz informacionnyh sistem, Tome 16 (2009) no. 1, pp. 92-111

Voir la notice de l'article provenant de la source Math-Net.Ru

Formal proving of program correctness is the only reliable method that ensures proper functioning of program systems. Existing verification methods are quite complicated in practice, that obstructs their extensive application. In this article an approach using “Design By Contract” conception is proposed, where class protocols formulated in terms of Petri nets makes it possible to analyze workability of classes and programs separately that facilitates the procedure of program correctness checking.
Keywords: programming languages, formal program verification, object-oriented programming, Petri nets. 
@article{MAIS_2009_16_1_a6,
     author = {D. I. Kharitonov},
     title = {Separable object-oriented program verification with {C++} class protocol definition in terms of {Petri} nets},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {92--111},
     publisher = {mathdoc},
     volume = {16},
     number = {1},
     year = {2009},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2009_16_1_a6/}
}
TY  - JOUR
AU  - D. I. Kharitonov
TI  - Separable object-oriented program verification with C++ class protocol definition in terms of Petri nets
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2009
SP  - 92
EP  - 111
VL  - 16
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2009_16_1_a6/
LA  - ru
ID  - MAIS_2009_16_1_a6
ER  - 
%0 Journal Article
%A D. I. Kharitonov
%T Separable object-oriented program verification with C++ class protocol definition in terms of Petri nets
%J Modelirovanie i analiz informacionnyh sistem
%D 2009
%P 92-111
%V 16
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2009_16_1_a6/
%G ru
%F MAIS_2009_16_1_a6
D. I. Kharitonov. Separable object-oriented program verification with C++ class protocol definition in terms of Petri nets. Modelirovanie i analiz informacionnyh sistem, Tome 16 (2009) no. 1, pp. 92-111. http://geodesic.mathdoc.fr/item/MAIS_2009_16_1_a6/