Specification Based Program Construction and Verification in Composition-Nominative Language CNLS

M.A. Bezverha, P.P. Protsyk

Abstract


This work continues the series of previous studies whose primary purpose was creating efficient languages, approaches and software tools for development of quality software systems using formal methods. On the basis of developed specification and programming languages we present new practical approaches for automated construction and verification of programs based on formal specifications. In particular, methods of conversion specifications in the program code, the use of special means of language to automatically create test cases and language capabilities for the application of run-time verification.

Problems in programming 2010; 2-3: 340-348


References


J.C. Knight, C.L. Dejong, M.S. Gibble, L.G. Nakano. Why Are Formal Methods Not Used More Widely // Fourth NASA Formal Methods

Workshop. – 1997. P. 1–12.

Процик П.П. Композиційно–номінативна мова програмування Script.NET // "Проблеми програмування". № 2–3 (спеціальний випуск). Київ – 2008. –С. 323–331.

Процик П.П. Композиційно-номінативний підхід до побудови семантики Z-Notation // Вісник київського університету. Сер.: Фізикоматематичні науки. – 2008. – № 1. – С. 116–120.

Процик П.П. Композиційно-номінативний підхід до специфікації програмних систем у мові Z-Notation // Вісник Київського

університету. Сер.: Фізіко-математичні науки.–2009.–№ 1. –С. 133–138.

Никитченко Н.С. Композиционно-номинативный подход к уточнению понятия программы. // Проблеми программування. – 1999.–№ 1. – C. 16– 31.

Нікітченко Н.С., Шкільняк С.С. Математична логіка та теорія алгоритмів:підручник – К.: Видавничо-поліграфічний центр «Київський університет», 2008. – 528 с.

Jim Woodcock, Jim Davies: Using Z. Specification, Refinement, and Proof // Prentice Hall, New York – 1996. – 523 p.

B. Meyer. Object-oriented software construction – New York: Prentice–Hall International Series of Computer Science, 2000. – 1296 p.

B. Meyer Eiffel: The Language– New York: Prentice–Hall International Series of Computer Science, 1992. – 296 p.

M. Barnett, K. Rustan, M. Leino, W. Schulte. The Spec# programming system: An Overview // CASSIS 2004 Proceedings – 2004. – P. 29–69.

Martin Andrew Relating Z and First-Order Logic // Journal of Formal Methods. – 1999. – Volume II. – P. 1266–1280.

Shengchao Qin; Guanhua He, Linking Object-Z with Spec# //Proc. of 12th IEEE International Conference on Engineering Complex Computer Systems, 11–14 July 2007. – P. 185 – 196.

L. Moura N. Bjørner, Z3: An Efficient SMT Solver, Conference on Tools and Algorithms for the Construction and Analysis of Systems

(TACAS), Budapest, Hungary, 2008. – P. 1–10.

B. Dutertre and L. Moura. The YICES SMT Solver. In SMTCOMP: Satisfiability Modulo Theories Competition, 2006.

M. Barnett and W. Schulte. Contracts, Components, and their Runtime Verification. Technical Report MSR–TR–2002–38, Microsoft Research, April 2002.


Refbacks

  • There are currently no refbacks.