检索结果-内蒙古大学图书馆

Property-Based Testing by Elaborating Proof Outlines

THEORY AND PRACTICE OF LOGIC PROGRAMMING 2024年第6期24卷 1123-1162页

作者： Miller, Dale Momigliano, Alberto Ecole Polytech INRIA Saclay Palaiseau France Ecole Polytech LIX Palaiseau France Univ Milan DI Milan Italy

Property-based testing (PBT) is a technique for validating code against an executable specification by automatically generating test-data. We present a proof-theoretical reconstruction of this style of testing for relational specifications and employ the Foundational Proof Certificate framework to describe test generators. We do this by encoding certain kinds of "proof outlines" as proof certificates that can describe various common generation strategies in the PBT literature, ranging from random to exhaustive, including their combination. We also address the shrinking of counterexamples as a first step toward their explanation. Once generation is accomplished, the testing phase is a standard logic programing search. After illustrating our techniques on simple, first-order (algebraic) data structures, we lift it to data structures containing bindings by using the lambda-tree syntax approach to encode bindings. The lambda Prolog programing language can perform both generating and checking of tests using this approach to syntax. We then further extend PBT to specifications in a fragment of linear logic.

关键词： property-based testing relational specifications meta-theory of programing languages lambda-tree syntax linear logic

来源：评论

学校读者我要写书评

暂无评论

A Lightweight Formalization of the Metatheory of Bisimulation-Up-To 15

A Lightweight Formalization of the Metatheory of Bisimulatio...

引用

ACM SIGPLAN Conference on Certified Programs and Proofs (CPP)

作者： Chaudhuri, Kaustuv Cimini, Matteo Miller, Dale INRIA Le Chesnay France Ecole Polytech LIX Palaiseau France Indiana Univ Bloomington IN 47405 USA

ISBN: (纸本)9781450332965

Bisimilarity of two processes is formally established by producing a bisimulation relation that contains those two processes and obeys certain closure properties. In many situations, particularly when the underlying labeled transition system is unbounded, these bisimulation relations can be large and even infinite. The bisimulation-up-to technique has been developed to reduce the size of the relations being computed while retaining soundness, that is, the guarantee of the existence of a bisimulation. Such techniques are increasingly becoming a critical ingredient in the automated checking of bisimilarity. This paper is devoted to the formalization of the meta theory of several major bisimulation-up-to techniques for the process calculi CCS and the pi-calculus (with replication). Our formalization is based on recent work on the proof theory of least and greatest fixpoints, particularly the use of relations defined (co-)inductively, and of co-inductive proofs about such relations, as implemented in the Abella theorem prover. An important feature of our formalization is that our definitions of the bisimulation-up-to relations are, in most cases, straightforward translations of published informal definitions, and our proofs clarify several technical details of the informal descriptions. Since the logic behind Abella also supports lambda-tree syntax and generic reasoning using the del-quantifier, our treatment of the pi-calculus is both direct and natural.

关键词： Bisimulation-up-to process calculus lambda-tree syntax co-induction Abella

来源：评论

学校读者我要写书评

暂无评论

A Two-Level Logic Approach to Reasoning About Computations

引用

JOURNAL OF AUTOMATED REASONING 2012年第2期49卷 241-273页

作者： Gacek, Andrew Miller, Dale Nadathur, Gopalan INRIA Saclay Ile de France Palaiseau France LIX Ecole Polytech Palaiseau France Univ Minnesota Dept Comp Sci & Engn Minneapolis MN 55455 USA

Relational descriptions have been used in formalizing diverse computational notions, including, for example, operational semantics, typing, and acceptance by non-deterministic machines. We therefore propose a (restricted) logical theory over relations as a language for specifying such notions. Our specification logic is further characterized by an ability to explicitly treat binding in object languages. Once such a logic is fixed, a natural next question is how we might prove theorems about specifications written in it. We propose to use a second logic, called a reasoning logic, for this purpose. A satisfactory reasoning logic should be able to completely encode the specification logic. Associated with the specification logic are various notions of binding: for quantifiers within formulas, for eigenvariables within sequents, and for abstractions within terms. To provide a natural treatment of these aspects, the reasoning logic must encode binding structures as well as their associated notions of scope, free and bound variables, and capture-avoiding substitution. Further, to support arguments about provability, the reasoning logic should possess strong mechanisms for constructing proofs by induction and co-induction. We provide these capabilities here by using a logic called which represents relations over lambda-terms via definitions of atomic judgments, contains inference rules for induction and co-induction, and includes a special generic quantifier. We show how provability in the specification logic can be transparently encoded in . We also describe an interactive theorem prover called Abella that implements and this two-level logic approach and we present several examples that demonstrate the efficacy of Abella in reasoning about computations.

关键词： Two-level logic Nominal abstraction Generic judgments del-quantification lambda-tree syntax

来源：评论

学校读者我要写书评

暂无评论

Nominal abstraction

引用

INFORMATION AND COMPUTATION 2011年第1期209卷 48-73页

作者： Gacek, Andrew Miller, Dale Nadathur, Gopalan Univ Minnesota Dept Comp Sci & Engn Minneapolis MN 55455 USA Ecole Polytech INRIA Saclay Ile de France & LIX F-91128 Palaiseau France

Recursive relational specifications are commonly used to describe the computational structure of formal systems. Recent research in proof theory has identified two features that facilitate direct, logic-based reasoning about such descriptions: the interpretation of atomic judgments through recursive definitions and an encoding of binding constructs via generic judgments. However, logics encompassing these two features do not currently allow for the definition of relations that embody dynamic aspects related to binding, a capability needed in many reasoning tasks. We propose a new relation between terms called nominal abstraction as a means for overcoming this deficiency. We incorporate nominal abstraction into a rich logic also including definitions, generic quantification, induction, and co-induction that we then prove to be consistent. We present examples to show that this logic can provide elegant treatments of binding contexts that appear in many proofs, such as those establishing properties of typing calculi and of arbitrarily cascading substitutions that play a role in reducibility arguments. (C) 2010 Elsevier Inc. All rights reserved.

关键词： Generic judgments Higher-order abstract syntax lambda-tree syntax Proof search Reasoning about operational semantics

来源：评论

学校读者我要写书评

暂无评论

Proof Search Specifications of Bisimulation and Modal Logics for the π-calculus

引用

ACM TRANSACTIONS ON COMPUTATIONAL LOGIC 2010年第2期11卷 13-13页

作者： Tiu, Alwen Miller, Dale Australian Natl Univ Coll Engn & Comp Sci Log & Computat Grp Canberra ACT 0200 Australia Ecole Polytech LIX F-91128 Palaiseau France INRIA Saclay Saclay France

We specify the operational semantics and bisimulation relations for the finite pi-calculus within a logic that contains the del quantifier for encoding generic judgments and definitions for encoding fixed points. Since we restrict to the finite case, the ability of the logic to unfold fixed points allows this logic to be complete for both the inductive nature of operational semantics and the coinductive nature of bisimulation. The del quantifier helps with the delicate issues surrounding the scope of variables within pi-calculus expressions and their executions (proofs). We illustrate several merits of the logical specifications permitted by this logic: they are natural and declarative;they contain no side-conditions concerning names of variables while maintaining a completely formal treatment of such variables;differences between late and open bisimulation relations arise from familar logic distinctions;the interplay between the three quantifiers (for all, there exists, and del) and their scopes can explain the differences between early and late bisimulation and between various modal operators based on bound input and output actions;and proof search involving the application of inference rules, unification, and backtracking can provide complete proof systems for one-step transitions, bisimulation, and satisfaction in modal logic. We also illustrate how one can encode the pi-calculus with replications, in an extended logic with induction and co-induction.

关键词： Theory Verification Proof search lambda-tree syntax del quantifier generic judgments higher-order abstract syntax pi-calculus bisimulation modal logics

来源：评论

学校读者我要写书评

暂无评论

Reasoning in Abella about Structural Operational Semantics Specifications

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2009年第C期228卷 85-100页

作者： Gacek, Andrew Miller, Dale Nadathur, Gopalan Univ Minnesota Dept Comp Sci & Engn Minneapolis MN 55455 USA INRIA Saclay Ile de France Palaiseau France LIX Ecole Polytech Palaiseau France

The approach to reasoning about structural operational semantics style specifications supported by the Abella system is discussed. This approach uses lambda-tree syntax to treat object language binding and encodes binding related properties in generic judgments. Further, object language specifications are embedded directly into the reasoning framework through recursive definitions. The treatment of binding via generic judgments implicitly enforces distinctness and atomicity in the names used for bound variables. These properties must, however, be made explicit in reasoning tasks. This objective can be achieved by allowing recursive definitions to also specify generic properties of atomic predicates. The utility of these various logical features in the Abella system is demonstrated through actual reasoning tasks. Brief comparisons with a few other logic based approaches are also made.

关键词： Structural operational semantics Abella lambda-tree syntax object language binding

来源：评论

学校读者我要写书评

暂无评论

A Proof Theoretic Approach to Operational Semantics

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2006年第1期162卷 243-247页

作者： Miller, Dale INRIA & LIX Ecole Polytech Palaiseau France

Proof theory can be applied to the problem of specifying and reasoning about the operational semantics of process calculi. We overview some recent research in which lambda-tree syntax is used to encode expressions containing bindings and sequent calculus is used to reason about operational semantics. There are various benefits of this proof theoretic approach for the pi-calculus: the treatment of bindings can be captured with no side conditions;bisimulation has a simple and natural specification in which the difference between bound input and bound output is characterized using difference quantifiers;various modal logics for mobility can be specified declaratively;and simple logic programming-like deduction involving subsets of second-order unification provides immediate implementations of symbolic bisimulation. These benefits should extend to other process calculi as well. As partial evidence of this, a simple lambda-tree syntax extension to the tyft/tyxt rule format for name-binding and name-passing is possible that allows one to conclude that (open) bisimilarity is a congruence.

关键词： operational semantics proof theoretic specifications lambda-tree syntax rule formats pi-calculus

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：