文章基本信息

标题：ENFORCe: A System for Ensuring Formal Correctness of High-level Programs
本地全文：下载
作者：Karl Azab ; Annegret Habel ; Karl-Heinz Pennemann 等
期刊名称：Electronic Communications of the EASST
电子版ISSN：1863-2122
出版年度：2006
卷号：1
期号：0
语种：English
出版社：European Association of Software Science and Technology (EASST)
摘要：Graph programs allow a visual description of programs on graphs and graph-like structures. The correctness of a graph program with respect to a pre- and a postcondition can be shown in a classical way by constructing a weakest precondition of the program relative to the postcondition and checking whether the precondition implies the weakest precondition. ENFORCe is a currently developed system for ensuring formal correctness of graph programs and, more general, high-level programs by computing weakest preconditions of these programs. In this paper, we outline the features of the system and present its software framework.