diff --git a/web/entries/BTree.html b/web/entries/BTree.html --- a/web/entries/BTree.html +++ b/web/entries/BTree.html @@ -1,207 +1,207 @@ A Verified Imperative Implementation of B-Trees - Archive of Formal Proofs

 

 

 

Home
About
Submission
Updating Entries
Using Entries
Search
Statistics
Index
Download

 

 

 

A Verified Imperative Implementation of B-Trees

 

Title: A Verified Imperative Implementation of B-Trees
Author: Niels Mündler (n /dot/ muendler /at/ tum /dot/ de)
Submission date: 2021-02-24
Abstract: In this work, we use the interactive theorem prover Isabelle/HOL to verify an imperative implementation of the classical B-tree data -structure invented by Bauer and McCreight [ACM 1970]. The +structure invented by Bayer and McCreight [ACM 1970]. The implementation supports set membership and insertion queries with efficient binary search for intra-node navigation. This is accomplished by first specifying the structure abstractly in the functional modeling language HOL and proving functional correctness. Using manual refinement, we derive an imperative implementation in Imperative/HOL. We show the validity of this refinement using the separation logic utilities from the Isabelle Refinement Framework . The code can be exported to the programming languages SML and Scala. We examine the runtime of all operations indirectly by reproducing results of the logarithmic relationship between height and the number of nodes. The results are discussed in greater detail in the corresponding Bachelor's Thesis.
BibTeX: 
@article{BTree-AFP,
   author  = {Niels Mündler},
   title   = {A Verified Imperative Implementation of B-Trees},
   journal = {Archive of Formal Proofs},
   month   = feb,
   year    = 2021,
   note    = {\url{https://isa-afp.org/entries/BTree.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }
License: BSD License
Depends on: Refine_Imperative_HOL

Proof outline
Proof document
Browse theories
Download this entry
Older releases: None
\ No newline at end of file diff --git a/web/rss.xml b/web/rss.xml --- a/web/rss.xml +++ b/web/rss.xml @@ -1,614 +1,614 @@ Archive of Formal Proofs https://www.isa-afp.org The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle. 24 Feb 2021 00:00:00 +0000 A Verified Imperative Implementation of B-Trees https://www.isa-afp.org/entries/BTree.html https://www.isa-afp.org/entries/BTree.html Niels Mündler 24 Feb 2021 00:00:00 +0000 In this work, we use the interactive theorem prover Isabelle/HOL to verify an imperative implementation of the classical B-tree data -structure invented by Bauer and McCreight [ACM 1970]. The +structure invented by Bayer and McCreight [ACM 1970]. The implementation supports set membership and insertion queries with efficient binary search for intra-node navigation. This is accomplished by first specifying the structure abstractly in the functional modeling language HOL and proving functional correctness. Using manual refinement, we derive an imperative implementation in Imperative/HOL. We show the validity of this refinement using the separation logic utilities from the <a href="https://www.isa-afp.org/entries/Refine_Imperative_HOL.html"> Isabelle Refinement Framework </a> . The code can be exported to the programming languages SML and Scala. We examine the runtime of all operations indirectly by reproducing results of the logarithmic relationship between height and the number of nodes. The results are discussed in greater detail in the corresponding <a href="https://mediatum.ub.tum.de/1596550">Bachelor's Thesis</a>. Formal Puiseux Series https://www.isa-afp.org/entries/Formal_Puiseux_Series.html https://www.isa-afp.org/entries/Formal_Puiseux_Series.html Manuel Eberl 17 Feb 2021 00:00:00 +0000 <p>Formal Puiseux series are generalisations of formal power series and formal Laurent series that also allow for fractional exponents. They have the following general form: \[\sum_{i=N}^\infty a_{i/d} X^{i/d}\] where <em>N</em> is an integer and <em>d</em> is a positive integer.</p> <p>This entry defines these series including their basic algebraic properties. Furthermore, it proves the Newton–Puiseux Theorem, namely that the Puiseux series over an algebraically closed field of characteristic 0 are also algebraically closed.</p> The Laws of Large Numbers https://www.isa-afp.org/entries/Laws_of_Large_Numbers.html https://www.isa-afp.org/entries/Laws_of_Large_Numbers.html Manuel Eberl 10 Feb 2021 00:00:00 +0000 <p>The Law of Large Numbers states that, informally, if one performs a random experiment $X$ many times and takes the average of the results, that average will be very close to the expected value $E[X]$.</p> <p> More formally, let $(X_i)_{i\in\mathbb{N}}$ be a sequence of independently identically distributed random variables whose expected value $E[X_1]$ exists. Denote the running average of $X_1, \ldots, X_n$ as $\overline{X}_n$. Then:</p> <ul> <li>The Weak Law of Large Numbers states that $\overline{X}_{n} \longrightarrow E[X_1]$ in probability for $n\to\infty$, i.e. $\mathcal{P}(|\overline{X}_{n} - E[X_1]| > \varepsilon) \longrightarrow 0$ as $n\to\infty$ for any $\varepsilon > 0$.</li> <li>The Strong Law of Large Numbers states that $\overline{X}_{n} \longrightarrow E[X_1]$ almost surely for $n\to\infty$, i.e. $\mathcal{P}(\overline{X}_{n} \longrightarrow E[X_1]) = 1$.</li> </ul> <p>In this entry, I formally prove the strong law and from it the weak law. The approach used for the proof of the strong law is a particularly quick and slick one based on ergodic theory, which was formalised by Gouëzel in another AFP entry.</p> Tarski's Parallel Postulate implies the 5th Postulate of Euclid, the Postulate of Playfair and the original Parallel Postulate of Euclid https://www.isa-afp.org/entries/IsaGeoCoq.html https://www.isa-afp.org/entries/IsaGeoCoq.html Roland Coghetto 31 Jan 2021 00:00:00 +0000 <p>The <a href="https://geocoq.github.io/GeoCoq/">GeoCoq library</a> contains a formalization of geometry using the Coq proof assistant. It contains both proofs about the foundations of geometry and high-level proofs in the same style as in high school. We port a part of the GeoCoq 2.4.0 library to Isabelle/HOL: more precisely, the files Chap02.v to Chap13_3.v, suma.v as well as the associated definitions and some useful files for the demonstration of certain parallel postulates. The synthetic approach of the demonstrations is directly inspired by those contained in GeoCoq. The names of the lemmas and theorems used are kept as far as possible as well as the definitions. </p> <p>It should be noted that T.J.M. Makarios has done <a href="https://www.isa-afp.org/entries/Tarskis_Geometry.html">some proofs in Tarski's Geometry</a>. It uses a definition that does not quite coincide with the definition used in Geocoq and here. Furthermore, corresponding definitions in the <a href="https://www.isa-afp.org/entries/Poincare_Disc.html">Poincaré Disc Model development</a> are not identical to those defined in GeoCoq. </p> <p>In the last part, it is formalized that, in the neutral/absolute space, the axiom of the parallels of Tarski's system implies the Playfair axiom, the 5th postulate of Euclid and Euclid's original parallel postulate. These proofs, which are not constructive, are directly inspired by Pierre Boutry, Charly Gries, Julien Narboux and Pascal Schreck. </p> Solution to the xkcd Blue Eyes puzzle https://www.isa-afp.org/entries/Blue_Eyes.html https://www.isa-afp.org/entries/Blue_Eyes.html Jakub Kądziołka 30 Jan 2021 00:00:00 +0000 In a <a href="https://xkcd.com/blue_eyes.html">puzzle published by Randall Munroe</a>, perfect logicians forbidden from communicating are stranded on an island, and may only leave once they have figured out their own eye color. We present a method of modeling the behavior of perfect logicians and formalize a solution of the puzzle. Hood-Melville Queue https://www.isa-afp.org/entries/Hood_Melville_Queue.html https://www.isa-afp.org/entries/Hood_Melville_Queue.html Alejandro Gómez-Londoño 18 Jan 2021 00:00:00 +0000 This is a verified implementation of a constant time queue. The original design is due to <a href="https://doi.org/10.1016/0020-0190(81)90030-2">Hood and Melville</a>. This formalization follows the presentation in <em>Purely Functional Data Structures</em>by Okasaki. JinjaDCI: a Java semantics with dynamic class initialization https://www.isa-afp.org/entries/JinjaDCI.html https://www.isa-afp.org/entries/JinjaDCI.html Susannah Mansky 11 Jan 2021 00:00:00 +0000 We extend Jinja to include static fields, methods, and instructions, and dynamic class initialization, based on the Java SE 8 specification. This includes extension of definitions and proofs. This work is partially described in Mansky and Gunter's paper at CPP 2019 and Mansky's doctoral thesis (UIUC, 2020). Cofinality and the Delta System Lemma https://www.isa-afp.org/entries/Delta_System_Lemma.html https://www.isa-afp.org/entries/Delta_System_Lemma.html Pedro Sánchez Terraf 27 Dec 2020 00:00:00 +0000 We formalize the basic results on cofinality of linearly ordered sets and ordinals and Šanin’s Lemma for uncountable families of finite sets. This last result is used to prove the countable chain condition for Cohen posets. We work in the set theory framework of Isabelle/ZF, using the Axiom of Choice as needed. Topological semantics for paraconsistent and paracomplete logics https://www.isa-afp.org/entries/Topological_Semantics.html https://www.isa-afp.org/entries/Topological_Semantics.html David Fuenmayor 17 Dec 2020 00:00:00 +0000 We introduce a generalized topological semantics for paraconsistent and paracomplete logics by drawing upon early works on topological Boolean algebras (cf. works by Kuratowski, Zarycki, McKinsey & Tarski, etc.). In particular, this work exemplarily illustrates the shallow semantical embeddings approach (<a href="http://dx.doi.org/10.1007/s11787-012-0052-y">SSE</a>) employing the proof assistant Isabelle/HOL. By means of the SSE technique we can effectively harness theorem provers, model finders and 'hammers' for reasoning with quantified non-classical logics. Relational Minimum Spanning Tree Algorithms https://www.isa-afp.org/entries/Relational_Minimum_Spanning_Trees.html https://www.isa-afp.org/entries/Relational_Minimum_Spanning_Trees.html Walter Guttmann, Nicolas Robinson-O'Brien 08 Dec 2020 00:00:00 +0000 We verify the correctness of Prim's, Kruskal's and Borůvka's minimum spanning tree algorithms based on algebras for aggregation and minimisation. Inline Caching and Unboxing Optimization for Interpreters https://www.isa-afp.org/entries/Interpreter_Optimizations.html https://www.isa-afp.org/entries/Interpreter_Optimizations.html Martin Desharnais 07 Dec 2020 00:00:00 +0000 This Isabelle/HOL formalization builds on the <em>VeriComp</em> entry of the <em>Archive of Formal Proofs</em> to provide the following contributions: <ul> <li>an operational semantics for a realistic virtual machine (Std) for dynamically typed programming languages;</li> <li>the formalization of an inline caching optimization (Inca), a proof of bisimulation with (Std), and a compilation function;</li> <li>the formalization of an unboxing optimization (Ubx), a proof of bisimulation with (Inca), and a simple compilation function.</li> </ul> This formalization was described in the CPP 2021 paper <em>Towards Efficient and Verified Virtual Machines for Dynamic Languages</em> The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols https://www.isa-afp.org/entries/Relational_Method.html https://www.isa-afp.org/entries/Relational_Method.html Pasquale Noce 05 Dec 2020 00:00:00 +0000 This paper introduces a new method for the formal verification of cryptographic protocols, the relational method, derived from Paulson's inductive method by means of some enhancements aimed at streamlining formal definitions and proofs, specially for protocols using public key cryptography. Moreover, this paper proposes a method to formalize a further security property, message anonymity, in addition to message confidentiality and authenticity. The relational method, including message anonymity, is then applied to the verification of a sample authentication protocol, comprising Password Authenticated Connection Establishment (PACE) with Chip Authentication Mapping followed by the explicit verification of an additional password over the PACE secure channel. Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information https://www.isa-afp.org/entries/Isabelle_Marries_Dirac.html https://www.isa-afp.org/entries/Isabelle_Marries_Dirac.html Anthony Bordg, Hanna Lachnitt, Yijun He 22 Nov 2020 00:00:00 +0000 This work is an effort to formalise some quantum algorithms and results in quantum information theory. Formal methods being critical for the safety and security of algorithms and protocols, we foresee their widespread use for quantum computing in the future. We have developed a large library for quantum computing in Isabelle based on a matrix representation for quantum circuits, successfully formalising the no-cloning theorem, quantum teleportation, Deutsch's algorithm, the Deutsch-Jozsa algorithm and the quantum Prisoner's Dilemma. The HOL-CSP Refinement Toolkit https://www.isa-afp.org/entries/CSP_RefTK.html https://www.isa-afp.org/entries/CSP_RefTK.html Safouan Taha, Burkhart Wolff, Lina Ye 19 Nov 2020 00:00:00 +0000 We use a formal development for CSP, called HOL-CSP2.0, to analyse a family of refinement notions, comprising classic and new ones. This analysis enables to derive a number of properties that allow to deepen the understanding of these notions, in particular with respect to specification decomposition principles for the case of infinite sets of events. The established relations between the refinement relations help to clarify some obscure points in the CSP literature, but also provide a weapon for shorter refinement proofs. Furthermore, we provide a framework for state-normalisation allowing to formally reason on parameterised process architectures. As a result, we have a modern environment for formal proofs of concurrent systems that allow for the combination of general infinite processes with locally finite ones in a logically safe way. We demonstrate these verification-techniques for classical, generalised examples: The CopyBuffer for arbitrary data and the Dijkstra's Dining Philosopher Problem of arbitrary size. Verified SAT-Based AI Planning https://www.isa-afp.org/entries/Verified_SAT_Based_AI_Planning.html https://www.isa-afp.org/entries/Verified_SAT_Based_AI_Planning.html Mohammad Abdulaziz, Friedrich Kurz 29 Oct 2020 00:00:00 +0000 We present an executable formally verified SAT encoding of classical AI planning that is based on the encodings by Kautz and Selman and the one by Rintanen et al. The encoding was experimentally tested and shown to be usable for reasonably sized standard AI planning benchmarks. We also use it as a reference to test a state-of-the-art SAT-based planner, showing that it sometimes falsely claims that problems have no solutions of certain lengths. The formalisation in this submission was described in an independent publication. AI Planning Languages Semantics https://www.isa-afp.org/entries/AI_Planning_Languages_Semantics.html https://www.isa-afp.org/entries/AI_Planning_Languages_Semantics.html Mohammad Abdulaziz, Peter Lammich 29 Oct 2020 00:00:00 +0000 This is an Isabelle/HOL formalisation of the semantics of the multi-valued planning tasks language that is used by the planning system Fast-Downward, the STRIPS fragment of the Planning Domain Definition Language (PDDL), and the STRIPS soundness meta-theory developed by Vladimir Lifschitz. It also contains formally verified checkers for checking the well-formedness of problems specified in either language as well the correctness of potential solutions. The formalisation in this entry was described in an earlier publication. A Sound Type System for Physical Quantities, Units, and Measurements https://www.isa-afp.org/entries/Physical_Quantities.html https://www.isa-afp.org/entries/Physical_Quantities.html Simon Foster, Burkhart Wolff 20 Oct 2020 00:00:00 +0000 The present Isabelle theory builds a formal model for both the International System of Quantities (ISQ) and the International System of Units (SI), which are both fundamental for physics and engineering. Both the ISQ and the SI are deeply integrated into Isabelle's type system. Quantities are parameterised by dimension types, which correspond to base vectors, and thus only quantities of the same dimension can be equated. Since the underlying "algebra of quantities" induces congruences on quantity and SI types, specific tactic support is developed to capture these. Our construction is validated by a test-set of known equivalences between both quantities and SI units. Moreover, the presented theory can be used for type-safe conversions between the SI system and others, like the British Imperial System (BIS). Finite Map Extras https://www.isa-afp.org/entries/Finite-Map-Extras.html https://www.isa-afp.org/entries/Finite-Map-Extras.html Javier Díaz 12 Oct 2020 00:00:00 +0000 This entry includes useful syntactic sugar, new operators and functions, and their associated lemmas for finite maps which currently are not present in the standard Finite_Map theory. A Formal Model of the Safely Composable Document Object Model with Shadow Roots https://www.isa-afp.org/entries/Shadow_SC_DOM.html https://www.isa-afp.org/entries/Shadow_SC_DOM.html Achim D. Brucker, Michael Herzberg 28 Sep 2020 00:00:00 +0000 In this AFP entry, we extend our formalization of the safely composable DOM with Shadow Roots. This is a proposal for Shadow Roots with stricter safety guarantess than the standard compliant formalization (see "Shadow DOM"). Shadow Roots are a recent proposal of the web community to support a component-based development approach for client-side web applications. Shadow roots are a significant extension to the DOM standard and, as web standards are condemned to be backward compatible, such extensions often result in complex specification that may contain unwanted subtleties that can be detected by a formalization. Our Isabelle/HOL formalization is, in the sense of object-orientation, an extension of our formalization of the core DOM and enjoys the same basic properties, i.e., it is extensible, i.e., can be extended without the need of re-proving already proven properties and executable, i.e., we can generate executable code from our specification. We exploit the executability to show that our formalization complies to the official standard of the W3C, respectively, the WHATWG. A Formal Model of the Document Object Model with Shadow Roots https://www.isa-afp.org/entries/Shadow_DOM.html https://www.isa-afp.org/entries/Shadow_DOM.html Achim D. Brucker, Michael Herzberg 28 Sep 2020 00:00:00 +0000 In this AFP entry, we extend our formalization of the core DOM with Shadow Roots. Shadow roots are a recent proposal of the web community to support a component-based development approach for client-side web applications. Shadow roots are a significant extension to the DOM standard and, as web standards are condemned to be backward compatible, such extensions often result in complex specification that may contain unwanted subtleties that can be detected by a formalization. Our Isabelle/HOL formalization is, in the sense of object-orientation, an extension of our formalization of the core DOM and enjoys the same basic properties, i.e., it is extensible, i.e., can be extended without the need of re-proving already proven properties and executable, i.e., we can generate executable code from our specification. We exploit the executability to show that our formalization complies to the official standard of the W3C, respectively, the WHATWG. A Formalization of Safely Composable Web Components https://www.isa-afp.org/entries/SC_DOM_Components.html https://www.isa-afp.org/entries/SC_DOM_Components.html Achim D. Brucker, Michael Herzberg 28 Sep 2020 00:00:00 +0000 While the (safely composable) DOM with shadow trees provide the technical basis for defining web components, it does neither defines the concept of web components nor specifies the safety properties that web components should guarantee. Consequently, the standard also does not discuss how or even if the methods for modifying the DOM respect component boundaries. In AFP entry, we present a formally verified model of safely composable web components and define safety properties which ensure that different web components can only interact with each other using well-defined interfaces. Moreover, our verification of the application programming interface (API) of the DOM revealed numerous invariants that implementations of the DOM API need to preserve to ensure the integrity of components. In comparison to the strict standard compliance formalization of Web Components in the AFP entry "DOM_Components", the notion of components in this entry (based on "SC_DOM" and "Shadow_SC_DOM") provides much stronger safety guarantees. A Formalization of Web Components https://www.isa-afp.org/entries/DOM_Components.html https://www.isa-afp.org/entries/DOM_Components.html Achim D. Brucker, Michael Herzberg 28 Sep 2020 00:00:00 +0000 While the DOM with shadow trees provide the technical basis for defining web components, the DOM standard neither defines the concept of web components nor specifies the safety properties that web components should guarantee. Consequently, the standard also does not discuss how or even if the methods for modifying the DOM respect component boundaries. In AFP entry, we present a formally verified model of web components and define safety properties which ensure that different web components can only interact with each other using well-defined interfaces. Moreover, our verification of the application programming interface (API) of the DOM revealed numerous invariants that implementations of the DOM API need to preserve to ensure the integrity of components. The Safely Composable DOM https://www.isa-afp.org/entries/Core_SC_DOM.html https://www.isa-afp.org/entries/Core_SC_DOM.html Achim D. Brucker, Michael Herzberg 28 Sep 2020 00:00:00 +0000 In this AFP entry, we formalize the core of the Safely Composable Document Object Model (SC DOM). The SC DOM improve the standard DOM (as formalized in the AFP entry "Core DOM") by strengthening the tree boundaries set by shadow roots: in the SC DOM, the shadow root is a sub-class of the document class (instead of a base class). This modifications also results in changes to some API methods (e.g., getOwnerDocument) to return the nearest shadow root rather than the document root. As a result, many API methods that, when called on a node inside a shadow tree, would previously ``break out'' and return or modify nodes that are possibly outside the shadow tree, now stay within its boundaries. This change in behavior makes programs that operate on shadow trees more predictable for the developer and allows them to make more assumptions about other code accessing the DOM. Syntax-Independent Logic Infrastructure https://www.isa-afp.org/entries/Syntax_Independent_Logic.html https://www.isa-afp.org/entries/Syntax_Independent_Logic.html Andrei Popescu, Dmitriy Traytel 16 Sep 2020 00:00:00 +0000 We formalize a notion of logic whose terms and formulas are kept abstract. In particular, logical connectives, substitution, free variables, and provability are not defined, but characterized by their general properties as locale assumptions. Based on this abstract characterization, we develop further reusable reasoning infrastructure. For example, we define parallel substitution (along with proving its characterizing theorems) from single-point substitution. Similarly, we develop a natural deduction style proof system starting from the abstract Hilbert-style one. These one-time efforts benefit different concrete logics satisfying our locales' assumptions. We instantiate the syntax-independent logic infrastructure to Robinson arithmetic (also known as Q) in the AFP entry <a href="https://www.isa-afp.org/entries/Robinson_Arithmetic.html">Robinson_Arithmetic</a> and to hereditarily finite set theory in the AFP entries <a href="https://www.isa-afp.org/entries/Goedel_HFSet_Semantic.html">Goedel_HFSet_Semantic</a> and <a href="https://www.isa-afp.org/entries/Goedel_HFSet_Semanticless.html">Goedel_HFSet_Semanticless</a>, which are part of our formalization of G&ouml;del's Incompleteness Theorems described in our CADE-27 paper <a href="https://dx.doi.org/10.1007/978-3-030-29436-6_26">A Formally Verified Abstract Account of Gödel's Incompleteness Theorems</a>. Robinson Arithmetic https://www.isa-afp.org/entries/Robinson_Arithmetic.html https://www.isa-afp.org/entries/Robinson_Arithmetic.html Andrei Popescu, Dmitriy Traytel 16 Sep 2020 00:00:00 +0000 We instantiate our syntax-independent logic infrastructure developed in <a href="https://www.isa-afp.org/entries/Syntax_Independent_Logic.html">a separate AFP entry</a> to the FOL theory of Robinson arithmetic (also known as Q). The latter was formalised using Nominal Isabelle by adapting <a href="https://www.isa-afp.org/entries/Incompleteness.html">Larry Paulson’s formalization of the Hereditarily Finite Set theory</a>. An Abstract Formalization of Gödel's Incompleteness Theorems https://www.isa-afp.org/entries/Goedel_Incompleteness.html https://www.isa-afp.org/entries/Goedel_Incompleteness.html Andrei Popescu, Dmitriy Traytel 16 Sep 2020 00:00:00 +0000 We present an abstract formalization of G&ouml;del's incompleteness theorems. We analyze sufficient conditions for the theorems' applicability to a partially specified logic. Our abstract perspective enables a comparison between alternative approaches from the literature. These include Rosser's variation of the first theorem, Jeroslow's variation of the second theorem, and the Swierczkowski&ndash;Paulson semantics-based approach. This AFP entry is the main entry point to the results described in our CADE-27 paper <a href="https://dx.doi.org/10.1007/978-3-030-29436-6_26">A Formally Verified Abstract Account of Gödel's Incompleteness Theorems</a>. As part of our abstract formalization's validation, we instantiate our locales twice in the separate AFP entries <a href="https://www.isa-afp.org/entries/Goedel_HFSet_Semantic.html">Goedel_HFSet_Semantic</a> and <a href="https://www.isa-afp.org/entries/Goedel_HFSet_Semanticless.html">Goedel_HFSet_Semanticless</a>. From Abstract to Concrete Gödel's Incompleteness Theorems—Part II https://www.isa-afp.org/entries/Goedel_HFSet_Semanticless.html https://www.isa-afp.org/entries/Goedel_HFSet_Semanticless.html Andrei Popescu, Dmitriy Traytel 16 Sep 2020 00:00:00 +0000 We validate an abstract formulation of G&ouml;del's Second Incompleteness Theorem from a <a href="https://www.isa-afp.org/entries/Goedel_Incompleteness.html">separate AFP entry</a> by instantiating it to the case of <i>finite consistent extensions of the Hereditarily Finite (HF) Set theory</i>, i.e., consistent FOL theories extending the HF Set theory with a finite set of axioms. The instantiation draws heavily on infrastructure previously developed by Larry Paulson in his <a href="https://www.isa-afp.org/entries/Incompleteness.html">direct formalisation of the concrete result</a>. It strengthens Paulson's formalization of G&ouml;del's Second from that entry by <i>not</i> assuming soundness, and in fact not relying on any notion of model or semantic interpretation. The strengthening was obtained by first replacing some of Paulson’s semantic arguments with proofs within his HF calculus, and then plugging in some of Paulson's (modified) lemmas to instantiate our soundness-free G&ouml;del's Second locale. From Abstract to Concrete Gödel's Incompleteness Theorems—Part I https://www.isa-afp.org/entries/Goedel_HFSet_Semantic.html https://www.isa-afp.org/entries/Goedel_HFSet_Semantic.html Andrei Popescu, Dmitriy Traytel 16 Sep 2020 00:00:00 +0000 We validate an abstract formulation of G&ouml;del's First and Second Incompleteness Theorems from a <a href="https://www.isa-afp.org/entries/Goedel_Incompleteness.html">separate AFP entry</a> by instantiating them to the case of <i>finite sound extensions of the Hereditarily Finite (HF) Set theory</i>, i.e., FOL theories extending the HF Set theory with a finite set of axioms that are sound in the standard model. The concrete results had been previously formalised in an <a href="https://www.isa-afp.org/entries/Incompleteness.html">AFP entry by Larry Paulson</a>; our instantiation reuses the infrastructure developed in that entry. A Formal Model of Extended Finite State Machines https://www.isa-afp.org/entries/Extended_Finite_State_Machines.html https://www.isa-afp.org/entries/Extended_Finite_State_Machines.html Michael Foster, Achim D. Brucker, Ramsay G. Taylor, John Derrick 07 Sep 2020 00:00:00 +0000 In this AFP entry, we provide a formalisation of extended finite state machines (EFSMs) where models are represented as finite sets of transitions between states. EFSMs execute traces to produce observable outputs. We also define various simulation and equality metrics for EFSMs in terms of traces and prove their strengths in relation to each other. Another key contribution is a framework of function definitions such that LTL properties can be phrased over EFSMs. Finally, we provide a simple example case study in the form of a drinks machine. Inference of Extended Finite State Machines https://www.isa-afp.org/entries/Extended_Finite_State_Machine_Inference.html https://www.isa-afp.org/entries/Extended_Finite_State_Machine_Inference.html Michael Foster, Achim D. Brucker, Ramsay G. Taylor, John Derrick 07 Sep 2020 00:00:00 +0000 In this AFP entry, we provide a formal implementation of a state-merging technique to infer extended finite state machines (EFSMs), complete with output and update functions, from black-box traces. In particular, we define the subsumption in context relation as a means of determining whether one transition is able to account for the behaviour of another. Building on this, we define the direct subsumption relation, which lifts the subsumption in context relation to EFSM level such that we can use it to determine whether it is safe to merge a given pair of transitions. Key proofs include the conditions necessary for subsumption to occur and that subsumption and direct subsumption are preorder relations. We also provide a number of different heuristics which can be used to abstract away concrete values into registers so that more states and transitions can be merged and provide proofs of the various conditions which must hold for these abstractions to subsume their ungeneralised counterparts. A Code Generator setup to create executable Scala code is also defined.