Industrial Experiences with a Formal DSL Semantics to Check the Correctness of DSL Artifacts
领域特定语言（DSL）从实现细节中抽象出来，并与领域专家对软件组件的推理方式保持一致。DSL的开发通常围绕生成实现代码或分析模型的语法和转换。语言的语义通常是隐式定义的，并根据实现代码的转换来定义。在存在来自DSL的多个转换的情况下，生成的工件相对于DSL的语义的正确性是一个相关的问题。我们表明，一个正式的语义是必不可少的检查生成的工件的正确性。我们利用工业项目中的形式语义，并使用基于等价性检查和基于模型的测试验证生成的工件的正确性的形式化技术。我们报告我们的经验，这种方法在一个工业发展项目。
2016-03-29 cs.LO cs.PL cs.SE
Transformation-Based Bottom-Up Computation of the Well-Founded Model
我们提出了一个框架，表达自自底向上的【形】的算法来计算良好的非析取逻辑程序的基础模型。我们的方法是基于黄铜和迪克斯的析取程序研究的条件事实和初等程序变换的概念。然而，即使我们限制他们的框架nondisjunctive程序，他们的剩余程序可以增长到指数大小，而对于无函数程序，我们的程序剩余部分总是多项式的扩展数据库（EDB）的大小。我们表明，我们的变换的特定顺序（我们称之为策略）对应于众所周知的计算方法，如交替不动点方法，有理有据的魔术集方法和魔术交替不动点程序。然而，由于我们的演算的汇合，我们提出了可证明比这些方法更好的有理模型的计算。与其他方法相比，我们的变换方法正确对待魔集变换的程序，即它总是计算原始程序的良基模型的相关部分。
2000-11-08 cs.LO
A Formalization of the Yul Language and Some Verified Yul Code Transformations
本文使用 ACL2 对 Solidity 编译器中间语言 Yul 的语法、语义及代码转换进行形式化，并证明静态与动态语义关系及转换正确性。
2025-07-25 cs.LO cs.PL
A Logic for Correlating Temporal Properties across Program Transformations
程序转换广泛应用于软件的综合、优化和维护。程序转换的正确性依赖于输入程序的一些重要性质的保持。通过把程序看作Kripke结构，程序的许多有趣的性质可以用时序逻辑来表达。在时序逻辑中，公式在单个程序上解释。然而，为了证明变换的正确性，我们会遇到包含一些子公式的公式，这些子公式在输入程序上解释，而在变换后的程序上解释。出现这种情况的一个例子是验证编译器应用的优化程序转换。在本文中，我们提出了一个逻辑称为时间转换逻辑（TTL）的原因，这样的公式。我们考虑不同类型的原始转换，并提出TTL推理规则。我们的程序转换和时序逻辑运算符的定义是新颖的，在他们使用的布尔矩阵代数。这导致了简洁和建设性的规范。此外，我们使用布尔矩阵代数在一个统一的方式来证明可靠的TTL推理规则。
2012-09-24 cs.LO cs.PL
Dynamic Magic Sets for Super-Consistent Answer Set Programs
在ASP的许多实际应用中，如数据集成、规划等，查询响应是非常重要的，因此ASP的查询优化技术是人们非常感兴趣的。魔术集是这些技术中的一种，最初是为Datasheet查询（没有析取和否定的ASP）定义的。动态魔术集（DMS）是这种技术的一个扩展，它已被证明是健全的和完整的查询回答ASP程序与分层否定。DMS的一个显着特点是，在ASP引擎的不确定性阶段也可以利用优化。特别是，在计算过程中做出一些假设之后，程序的某些部分可能会变得与这些假设下的查询无关。这允许搜索空间的动态修剪，这可能导致指数性能增益。本文对超一致ASP程序类（ASP^{sc}程序）进行了勇敢谨慎推理，形式化地建立并证明了DMS的正确性。ASP^{sc}程序保证一致性（即，有答案集），当一组任意的事实被添加到其中时。这一结果推广了DMS的适用性，因为ASP^{sc}程序的类比具有分层否定的ASP程序更丰富，特别是包括所有无奇循环的程序。DMS已被实现为DLV的扩展，DMS的有效性，ASP^{sc}程序的经验证实了与该系统的实验结果。
2010-11-19 cs.LO
Program Derivation by Correctness Enhacements
相对正确性是一个程序相对于给定规范比另一个程序更正确的属性。在相对正确性的许多性质中，我们发现最有趣的是程序P'精化程序P的性质，当且仅当P'在任何规范方面比P更正确。这启发我们通过连续的精化来重新考虑程序推导：这个过程的每一步都要求我们将程序P转换为精化P的程序P'，即P'在任何规范方面都比P更正确。这就提出了一个问题：当我们只需要满足规格R时，为什么我们要使P'在任何规格方面都比P更正确呢？在本文中，我们讨论了一个过程中的程序推导，取代传统的序列的基于细化的正确性保持转换从规格R开始的序列的相对正确性为基础的正确性增强转换从中止。
2016-06-07 cs.LO cs.SE
Verification of Imperative Programs by Constraint Logic Program Transformation
本文提出了一种基于约束逻辑程序变换（CLP）的方法来验证操作整数和数组的命令式程序的部分正确性。我们使用CLP作为一种元语言来表示命令式程序，它们的执行和它们的属性。首先，我们将命令式程序的正确性编码为CLP程序T定义的谓词“不正确”的否定。通过构造，“不正确”在T的最小模型中成立，当且仅当从初始配置执行prog最终在错误配置中停止。然后，我们对程序T应用一系列保持其最小模型语义的变换。这些转换是基于众所周知的转换规则，如展开和折叠，由适当的转换策略，如专业化和泛化。转换的目的是导出一个新的CLP程序TransfT，其中谓词“不正确”由以下定义：（i）事实“不正确”。'（在这种情况下prog是不正确的），或者由（ii）空子句集（在这种情况下prog是正确的）。在我们导出CLP程序使得（i）和（ii）都不成立的情况下，我们对变换进行了简化。由于问题是不可判定的，这个过程可能不会终止。我们通过例子表明，我们的方法可以应用在一个相当系统的方式，是适合自动化的程序验证领域的许多技术开发的程序转换。
2013-09-20 cs.LO cs.PL
Proving Correctness of Imperative Programs by Linearizing Constrained Horn Clauses
本文提出了一种基于规范自动转换的命令式程序正确性验证方法。给定一个程序prog，我们考虑形式为$\{φ\}$ prog $\{ψ\}$的部分正确性规范，其中断言$φ$和$ψ$是由可能递归的Horn子句的集合Spec定义的谓词，其前提中具有线性算术（LA）约束（也称为约束Horn子句）。验证方法包括在构造一组PC的约束Horn子句，其可满足性意味着$\{φ\}$ prog $\{ψ\}$是有效的。我们强调了一些限制的国家的最先进的约束霍恩子句求解方法，这里称为LA求解方法，证明可满足性的条款，通过寻找线性算术解释的谓词。特别是，我们证明了存在一些规格，不能证明有效的任何这些LA解决方法。这些规范要求证明一组包含非线性子句（即前提中有多个原子的子句）的受约束Horn子句的PC的可满足性。然后，我们提出了一个转换，称为线性化，PC转换成一组线性条款（即条款，在其前提中最多一个原子）。我们表明，几个规格，不能被证明是有效的LA解决方法，可以被证明是有效的线性化后。我们还提出了一种策略，用于执行线性化在一个自动的方式，我们报告的一些实验结果，通过使用我们的方法的初步实施。
2015-07-21 cs.LO cs.PL
Formal Model-Driven Engineering: Generating Data and Behavioural Components
模型驱动工程是从结构和功能的抽象模型中自动生成软件产品。通过针对特定的系统类别，可以使用模型转换和编码领域知识和实现策略的代码生成器来自动化开发过程的各个方面。使用这种方法，一个复杂的软件系统的正确性问题可以通过分析较低复杂性的抽象模型来回答，假设所采用的转换和生成器本身是正确的。本文展示了如何形式化技术可以用来建立模型转换的正确性，用于从精确的对象模型生成软件组件。源语言基于现有的形式化技术;目标语言是数据库编程中广泛使用的SQL表示法。正确性是通过为两种语言提供可比较的关系语义，并检查转换是否保持语义来建立的。
2013-01-01 cs.LO cs.MS cs.SE
Towards a General Framework for Formal Reasoning about Java Bytecode Transformation
程序转换引起了广泛的兴趣，因为它用于多种目的：改变程序的语义、向程序添加功能或执行优化。在本文中，我们专注于程序转换在字节码级别。由于这些转换可能会引入错误，因此我们的目标是提供一种正式的方法来验证更新并确定其正确性。提出的形式化框架定义了更新的形式语义，作为静态验证的基础，并提出了一种基于Hoare三元组和最弱前提演算的字节码转换行为推理方案
2013-07-31 cs.LO cs.PL
Verification of Object-Oriented Programs: a Transformational Approach
我们表明，验证面向对象的程序，通过断言的方法，可以实现在一个简单的方式，通过利用一个语法导向的转换，从面向对象的程序递归程序。这种转换表明自然的证明规则和它的正确性，帮助我们建立健全和相对完整的证明系统。困难之一是如何在断言语言中正确处理实例变量和别名。所讨论的程序设计语言支持数组、实例变量、失败和带参数的递归方法。
2011-11-08 cs.LO cs.PL
A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs
我们描述了一种方法来验证实现的转换功能的程序，利用高阶表示的语法。在这种方法中，使用遗传Harrop公式的逻辑指定变换。一方面，这些规范直接作为实现，是Lambda Prolog语言中的程序。另一方面，它们可以用作Abella系统的输入，该系统允许我们证明关于它们的属性，从而证明关于实现的属性。我们认为，这种方法是特别有效的实现转换，分析绑定结构。我们通过在Lambda Prolog中描述对这种结构敏感的类型化闭包转换和代码提升等转换的简洁编码，并通过展示如何使用Abella证明其正确性来做到这一点。
2016-01-23 cs.LO cs.PL
Magic Sets for Disjunctive Datalog Programs
University of Calabria（卡拉布里亚大学）
本文提出了一种新的技术，优化的（部分）绑定查询的析取数据库程序与分层否定。该技术利用查询绑定的传播，并扩展了魔术集（MS）优化技术。析取数据库的一个重要特性是非单调性，这需要非确定性的实现，例如回溯搜索。新方法的一个显着特点是，优化也可以利用在不确定性阶段。特别是，在计算过程中做出一些假设之后，程序的某些部分可能会变得与这些假设下的查询无关。这允许动态修剪搜索空间。相比之下，先前定义的用于析取数据库的MS方法的效果仅限于该过程的确定性部分。以这种方式，通过使用所提出的方法的潜在性能增益可以是指数的，如可以凭经验观察到的。MS的正确性是由于MS和无根据集之间的强关系建立的，这在以前的文献中还没有研究过。这种知识允许扩展的方法也以自然的方式与分层否定的程序。该方法已在DLV中实现，并进行了各种实验。合成数据上的实验结果证实了MS在析取数据处理中的实用性，并且它们突出了新方法可以获得的计算增益。先前提出的用于析取数据库程序的MS方法。对真实世界数据的进一步实验显示了MS在近年来受到相当关注的应用场景中的好处，回答可能不一致的数据库上的用户查询的问题源于自主信息源的集成。
2012-04-27 cs.AI cs.LO
Assembling the Proofs of Ordered Model Transformations
在模型驱动开发中，有序模型转换是源类和目标类之间的一组嵌套转换，其中每个转换由其自身的前置和后置条件控制，但在结构上依赖于其父级。在本文中，我们考虑的形式化建设性的类型论的概念模型和模型转换，并显示如何正确性证明潜在的大型有序模型转换可以系统地组装从证明其部分的规格，使它们更容易得到。
2013-02-21 cs.LO
Logic + control: On program construction and verification
本文提出了一个例子，形式化推理的语义Prolog程序的实际意义（SAT求解器的豪和国王）。该程序被视为一个带有附加控制的定子句逻辑程序。逻辑程序是通过逐步精化的方法构造的，并与其正确性和完整性证明携手并进。证明是声明性的--它们不引用任何操作语义。逻辑程序构造的每一步都遵循一种系统的方法来构造可证明正确和完整的程序。我们还证明了在最终的Prolog程序中保持了逻辑程序的正确性和完整性。此外，我们证明终止，发生检查自由和非挣扎。我们的例子展示了如何将处理“逻辑”和处理“控制”分开。大多数证明都可以在“逻辑”级别上完成，从任何操作语义中抽象出来。这个例子使用了近似的规格说明;它们在简化逻辑程序的推理中是至关重要的。它还表明，语义保持程序转换的范例可能是不够的。我们建议考虑转换保持正确性和完整性方面的近似规范。
2017-05-12 cs.LO cs.PL
Proving Equivalence Between Imperative and MapReduce Implementations Using Program Transformations
分布式程序通常在MapReduce、Spark和Thrill等流行的功能框架中制定，但为此类框架编写高效的算法通常是一项不平凡的任务。由于大规模运行错误算法的成本可能很高，因此非常需要验证它们的正确性。我们建议采用现有的命令式参考实现作为MapReduce实现的规范。为此，我们提出了一种新的验证方法，其中一个命令和MapReduce实现之间的等价性建立了一系列的程序转换。在本文中，我们提出了如何等价框架可以用来证明之间的等价性的PageRank算法和MapReduce变种的强制性实现。八个单独的转换步骤分别介绍和解释。
2018-03-27 cs.LO cs.PL
Reasoning about Graph Programs
GP 2是一种通过图形转换进行计算的非确定性程序设计语言。GP 2的设计目标之一是语法和语义的简单性，以促进程序的形式化推理。在本文中，我们演示了四个案例研究程序员如何证明终止和部分正确的解决方案。我们认为，GP 2的图形转换规则，连同感应程序执行的长度，提供了一个方便的框架程序验证。
2016-09-13 cs.LO cs.PL
Transformational Verification of Quicksort
为约束逻辑程序开发的许多转换技术，也称为约束Horn子句（CHC），在程序验证领域中找到了新的有用的应用。在本文中，我们通过基于转换的验证方法进行了一个非平凡的案例研究。我们认为熟悉的Quicksort程序排序列表，写在一个功能性的程序设计语言，我们验证的前/后置条件，指定预期的正确性属性的功能中定义的程序。我们通过以下方式验证这些属性：（1）将它们转换为CHC，（2）通过删除所有列表出现来转换CHC，以及（3）通过使用布尔和整数的Eldarica求解器来检查转换后的CHC的可满足性。在第（2）点提到的转换需要对以前工作中提出的消除归纳定义的数据结构的算法进行扩展，因为在转换的一个阶段，我们使用在以前阶段已经证明的一些性质作为引理。
2020-08-07 cs.LO cs.PL
Transformations of Logic Programs with Goals as Arguments
我们考虑逻辑编程的一个简单扩展，其中变量可以在目标上变化，目标可以是谓词的参数。在这种语言中，我们可以编写以目标为数据的逻辑程序。我们给出了实际的证据表明，利用这种能力时，转换程序，我们可以提高程序的效率。我们提出了一套程序转换规则，扩展了熟悉的展开和折叠规则，并允许我们操纵的目标出现的谓词参数的条款。为了证明这些转换规则的正确性，我们形式化地定义了我们的扩展逻辑程序设计语言的操作语义。这个语义是LD-分辨率的一个简单变体。当适当的条件得到满足时，这种语义与LD-分辨率一致，因此，用我们的扩展语言编写的程序可以由普通的Prolog系统运行。我们的转换规则，以保持操作语义和终止。
2004-02-20 cs.LO cs.PL
Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction
霍尔逻辑的证明表是一个带有前置和后置条件的带注释程序，它对应于霍尔逻辑的一棵推理树。在本文中，我们证明了部分正确性的证明表可以转化为一个推理序列的重写归纳约束重写。我们还表明，如果从程序获得的约束重写系统正在终止，则所得序列是对应于霍尔三重组的归纳定理的有效证明。这样一个有效的证明与终止的约束重写系统意味着完全正确的程序w.r.t.霍尔三人组转换，使我们能够应用技术证明终止约束重写证明总正确性的程序连同证明表格的部分正确性。
2018-02-19 cs.LO
Removing Unnecessary Variables from Horn Clause Verification Conditions
验证条件（Verification Conditions，VC）是一种逻辑公式，其可满足性保证了程序的正确性。我们认为VC的形式约束霍恩条款（CHC），这是自动生成的编码（解释器）的程序设计语言的操作语义。VC是通过基于展开/折叠变换规则的程序专门化而得到的，并且正如在专门化解释器时经常发生的那样，它们包含不必要的变量，即，在验证下的程序的正确性证明不需要的变量。在本文中，我们适应的CHC设置的一些技术，开发用于删除不必要的变量，从逻辑程序，我们表明，在某些情况下，这些技术的应用增加了霍恩子句求解器的有效性时，证明程序的正确性。
2016-07-15 cs.LO cs.PL cs.SE
Verifying Procedural Programs via Constrained Rewriting Induction
本文提出将过程式程序转换为逻辑约束项重写系统，通过扩展重写归纳方法自动验证内存安全性和函数正确性，并证明实现间等价性，无需单独规范语言。
2025-08-29 cs.LO
