ДЕДУКТИВНАЯ ВЕРИФИКАЦИЯ И РЕАЛИЗАЦИЯ ПРЕДИКАТНОЙ ПРОГРАММЫ ИНВЕРТИРОВ… · LibMeta · SciLib
IMT journal IMT journal articlePublicationAcademic article

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

http://libmeta.ru/object/imt_pub_260

Abstract

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

Данные

pages0-8
year2018
pageEnd8
pageStart0

author

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

topic

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

cites

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

references

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

keyword

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

UDC

004.43

in journal

Information and mathematical technologies in science and management

published in

ИМТ № 3(11) / 2018

part of

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

has fragment

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

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

← contains article · 1
Information and mathematical technologies in science and management
← fragment of · 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
← has part · 1
Information and mathematical technologies in science and management

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