Верификация С-программ является актуальной проблемой современного программирования. Для применения известных методов дедуктивной верификации необходимо аннотировать циклы посредством инвариантов, что во многих случаях является трудной задачей. В этой статье мы рассматриваем язык C-light, который является выразительным подмножеством языка C, соответствующего стандарту ISO. Для верификации C-light программ нами были предложены двухуровневый подход [19, 20] и метод смешанной аксиоматической семантики [1, 3, 11]. На первой стадии этого подхода исходная C-light программа транслируется [17] в программу на языке C-kernel [19], который является подмножеством языка C-light. Теорема о корректности этой трансляции была доказана в [10, 11]. По сравнению с C-light в языке C-kernel меньше операторов, что позволяет уменьшить число правил вывода при разработке аксиоматической семантики. На второй стадии этого подхода для программ на языке C-kernel порождаются условия корректности по правилам смешанной аксиоматической семантики [10, 11], которая может содержать несколько правил вывода для одной и той же программной конструкции. В таких случаях правила вывода применяются однозначно в зависимости от контекста. Заметим, что во многих случаях использование смешанной аксиоматической семантики позволяет упростить условия корректности. В этой статье представлено расширение данного подхода, которое включает наш метод верификации для финитной итерации над неизменяемыми структурами данных без выхода из тела цикла в C-light программах. Данный метод содержит новое правило вывода для таких финитных итераций без инвариантов. Это правило было реализовано в генераторе условий корректности. На стадии доказательства используется SMT-решатель Z3 [12]. Рассмотрен пример, иллюстрирующий применение данного подхода.
Статья представляет собой расширенную версию доклада на VI Международном семинаре “Program Semantics, Specification and Verification: Theory and Applications”, Казань, 2015.
Статья публикуется в авторской редакции.
The C-program verification is an urgent problem of modern programming. To apply known methods of deductive verification it is necessary to provide loop invariants which might be a challenge in many cases. In this paper we consider the C-light language [18] which is a powerful subset of the ISO C language. To verify C-light programs the two-level approach [19, 20] and the mixed axiomatic semantics method [1, 3, 11] were suggested. At the first stage, we translate [17] the source C-light program into Ckernel one. The C-kernel language [19] is a subset of C-light. The theorem of translation correctness was proved in [10, 11]. The C-kernel has less statements with respect to the C-light, this allows to decrease the number of inference rules of axiomatic semantics during its development. At the second stage of this approach, the verification conditions are generated by applying the rules of mixed axiomatic semantics [10, 11] which could contain several rules for the same program statement. In such cases the inference rules are applied depending on the context. Let us note that application of the mixed axiomatic semantics allows to significantly simplify verification conditions in many cases. This article represents an extension of this approach which includes our verification method for definite iteration over unchangeable data structures without loop exit in C-light programs. The method contains a new inference rule for the deifinite iteration without invariants. This rule was implemented in verification conditions generator. At the proof stage the SMT-solver Z3 [12] is used. An example which illustrates the application of this technique is considered.
he article is published in the authors’ wording.