ДЕДУКТИВНАЯ ВЕРИФИКАЦИЯ И РЕАЛИЗАЦИЯ ПРЕДИКАТНОЙ ПРОГРАММЫ ИНВЕРТИРОВ… · LibMeta · SciLib
Журнал ИМТ Статья журнала ИМТПубликацияНаучная статья

ДЕДУКТИВНАЯ ВЕРИФИКАЦИЯ И РЕАЛИЗАЦИЯ ПРЕДИКАТНОЙ ПРОГРАММЫ ИНВЕРТИРОВАНИЯ СПИСКОВ

http://libmeta.ru/object/imt_pub_260

Аннотация

Представлен метод предикатного программирования в применении к известной программе и нвертирования односвязных списков. Данная программа признана крайне трудн ой для дедуктивной верификации ( verification challenge ). Описыва ются построение и дедуктивная верификация предикатной программы инвертирования списка как объекта алгебраического типа. Эффективная императивная программа получена применением оптимизирующих трансформаций. Дедуктивная верификация предикатной программы на порядок проще верификации аналогичной императивной программы, использующей указатели.

Данные

pages0-8
год2018
pageEnd8
pageStart0

автор

Сороковиков Павел Сергеевич

тема

алгебраические типы данных дедуктивная верификация трансформации программ односвязный список 004.43

цитирует

An axiomatic basis for computer programming PVS Specification and Verification System Reasoning about Separation Using Abstraction and Reification Region analysis for deductive verification of C programs Separation Logic: A Logic for Shared Mutable Data Structures Specification and verification of object-oriented software Taking Parnas's Principles to the Next Level: Declarative Language Design The Dafny Integrated Development Environment Towards a Calculus of Object Programs Verification and Synthesis of Addition Programs under the Rules of Correctness … Верификация и синтез эффективных программ стандартных функций в технологии пред… Доказательное построение, верификация и синтез предикатных программ +15

ссылается на

An axiomatic basis for computer programming PVS Specification and Verification System Reasoning about Separation Using Abstraction and Reification Region analysis for deductive verification of C programs Separation Logic: A Logic for Shared Mutable Data Structures Specification and verification of object-oriented software Taking Parnas's Principles to the Next Level: Declarative Language Design The Dafny Integrated Development Environment Towards a Calculus of Object Programs Verification and Synthesis of Addition Programs under the Rules of Correctness … Верификация и синтез эффективных программ стандартных функций в технологии пред… Доказательное построение, верификация и синтез предикатных программ +15

ключевое слово

алгебраические типы данных дедуктивная верификация трансформации программ односвязный список

УДК

004.43

в журнале

Information and mathematical technologies in science and management

опубликовано в

ИМТ № 3(11) / 2018

часть

Information and mathematical technologies in science and management ИМТ № 3(11) / 2018

содержит фрагмент

260_0 260_1 260_2 260_3 260_4 260_5 260_6 260_7 260_8 260_9

Входящие связи

← содержит статью · 1
Information and mathematical technologies in science and management
← фрагмент статьи · 10
260_0 260_1 260_2 260_3 260_4 260_5 260_6 260_7 260_8 260_9
← Contains · 1
Information and mathematical technologies in science and management
← содержит · 1
Information and mathematical technologies in science and management

Внешние ссылки