Email Gateway (Aug 18 2022 at 19:06): Email Gateway (Aug 18 2022 at 19:06):From: Gerwin Klein <gerwin.klein@nicta.com.au>
[http://afp.sourceforge.net/entries/Refine_Monadic.shtml]
Refinement for Monadic Programs
by Peter Lammich
Abstract:
We provide a framework for program and data refinement in Isabelle/HOL. The framework is based on a nondeterminism-monad with assertions, i.e., the monad carries a set of results or an assertion failure. Recursion is expressed by fixed points. For convenience, we also provide while and foreach combinators.
The framework provides tools to automatize canonical tasks, such as verification condition generation, finding appropriate data refinement relations, and refine an executable program to a form that is accepted by the Isabelle/HOL code generator.
This submission comes with a collection of examples and a user-guide, illustrating the usage of the framework.
[http://afp.sourceforge.net/entries/Dijkstra_Shortest_Path.shtml]
Dijkstra's Shortest Path Algorithm
by Benedikt Nordhoff and Peter Lammich
Abstract:
We implement and prove correct Dijkstra's algorithm for the single source shortest path problem, conceived in 1956 by E. Dijkstra. The algorithm is implemented using the data refinement framework for monadic, nondeterministic programs. An efficient implementation is derived using data structures from the Isabelle Collection Framework.
Cheers,
Gerwin
Email Gateway (Aug 19 2022 at 12:32):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Two new AFP entries are available from [http://afp.sf.net]:
Gödel's Incompleteness Theorems
by Larry Paulson
Gödel's two incompleteness theorems are formalised, following a careful presentation by Swierczkowski, in the theory of hereditarily finite sets. This represents the first ever machine-assisted proof of the second incompleteness theorem. Compared with traditional formalisations using Peano arithmetic (see e.g. Boolos), coding is simpler, with no need to formalise the notion of multiplication (let alone that of a prime number) in the formalised calculus upon which the theorem is based. However, other technical problems had to be solved in order to complete the argument.
The Hereditarily Finite Sets
by Larry Paulson
The theory of hereditarily finite sets is formalised, following the development of Swierczkowski. An HF set is a finite collection of other HF sets; they enjoy an induction principle and satisfy all the axioms of ZF set theory apart from the axiom of infinity, which is negated. All constructions that are possible in ZF set theory (Cartesian products, disjoint sums, natural numbers, functions) without using infinite sets are possible here. The definition of addition for the HF sets follows Kirby. This development forms the foundation for the Isabelle proof of Gödel's incompleteness theorems, which has been formalised separately.
Enjoy,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 14:33):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Transitive closure according to Roy-Floyd-Warshall
by Makarius Wenzel
This formulation of the Roy-Floyd-Warshall algorithm for the
transitive closure bypasses matrices and arrays, but uses a more direct
mathematical model with adjacency functions for immediate predecessors and
successors. This can be implemented efficiently in functional programming
languages and is particularly adequate for sparse relations.
[http://afp.sf.net/entries/Roy_Floyd_Warshall.shtml]
Noninterference Security in Communicating Sequential Processes
by Pasquale Noce
An extension of classical noninterference security for deterministic
state machines, as introduced by Goguen and Meseguer and elegantly
formalized by Rushby, to nondeterministic systems should satisfy two
fundamental requirements: it should be based on a mathematically precise
theory of nondeterminism, and should be equivalent to (or at least not
weaker than) the classical notion in the degenerate deterministic case.
This paper proposes a definition of noninterference security applying
to Hoare's Communicating Sequential Processes (CSP) in the general case of
a possibly intransitive noninterference policy, and proves the
equivalence of this security property to classical noninterference
security for processes representing deterministic state machines.
Furthermore, McCullough's generalized noninterference security is shown
to be weaker than both the proposed notion of CSP noninterference security
for a generic process, and classical noninterference security for processes
representing deterministic state machines. This renders CSP noninterference
security preferable as an extension of classical noninterference security
to nondeterministic systems.
[http://afp.sf.net/entries/Noninterference_CSP.shtml]
Enjoy!
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 09:12):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO
by Peter Gammie, Tony Hosking, and Kai Engelhardt
Abstract:
We use ConcurrentIMP to model Schism, a state-of-the-art real-time
garbage collection scheme for weak memory, and show that it is safe
on x86-TSO.
This development accompanies the PLDI 2015 paper of the same name.
http://afp.sf.net/entries/ConcurrentGC.shtml
Concurrent IMP
by Peter Gammie
Abstract:
ConcurrentIMP extends the small imperative language IMP with control
non-determinism and constructs for synchronous message passing.
http://afp.sf.net/entries/ConcurrentIMP.shtml
Enjoy!
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 13:26):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Two new entries are available at http://isa-afp.org/
POSIX Lexing with Derivatives of Regular Expressions
by Fahad Ausaf, Roy Dyckhoff, and Christian Urban
Brzozowski introduced the notion of derivatives for regular
expressions. They can be used for a very simple regular expression
matching algorithm. Sulzmann and Lu cleverly extended this algorithm
in order to deal with POSIX matching, which is the underlying
disambiguation strategy for regular expressions needed in lexers. In
this entry we give our inductive definition of what a POSIX value is
and show (i) that such a value is unique (for given regular expression
and string being matched) and (ii) that Sulzmann and Lu's
algorithm always generates such a value (provided that the regular
expression matches the string). We also prove the correctness of an
optimised version of the POSIX matching algorithm.
Cardinality of Equivalence Relations
by Lukas Bulwahn
This entry provides formulae for counting the number of equivalence
relations and partial equivalence relations over a finite carrier set
with given cardinality. To count the number of equivalence relations,
we provide bijections between equivalence relations and set
partitions, and then transfer the main results of the two AFP entries,
Cardinality of Set Partitions and Spivey's Generalized Recurrence
for Bell Numbers, to theorems on equivalence relations. To count the
number of partial equivalence relations, we observe that counting
partial equivalence relations over a set A is equivalent to counting
all equivalence relations over all subsets of the set A. From this
observation and the results on equivalence relations, we show that the
cardinality of partial equivalence relations over a finite set of
cardinality n is equal to the n+1-th Bell number.
Enjoy!
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 13:28):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Two new entries are available from https://isa-afp.org :
Category Theory with Adjunctions and Limits
by Eugene W. Stark
This article attempts to develop a usable framework for doing category theory in Isabelle/HOL. Our point of view, which to some extent differs from that of the previous AFP articles on the subject, is to try to explore how category theory can be done efficaciously within HOL, rather than trying to match exactly the way things are done using a traditional approach. To this end, we define the notion of category in an "object-free" style, in which a category is represented by a single partial composition operation on arrows. This way of defining categories provides some advantages in the context of HOL, including the ability to avoid the use of records and the possibility of defining functors and natural transformations simply as certain functions on arrows, rather than as composite objects. We define various constructions associated with the basic notions, including: dual category, product category, functor category, discrete category, free category, functor composition, and horizontal and vertical composite of natural transformations. A "set category" locale is defined that axiomatizes the notion "category of all sets at a type and all functions between them," and a fairly extensive set of properties of set categories is derived from the locale assumptions. The notion of a set category is used to prove the Yoneda Lemma in a general setting of a category equipped with a "hom embedding," which maps arrows of the category to the "universe" of the set category. We also give a treatment of adjunctions, defining adjunctions via left and right adjoint functors, natural bijections between hom-sets, and unit and counit natural transformations, and showing the equivalence of these definitions. We also develop the theory of limits, including representations of functors, diagrams and cones, and diagonal functors. We show that right adjoint functors preserve limits, and that limits can be constructed via products and equalizers. We characterize the conditions under which limits exist in a set category. We also examine the case of limits in a functor category, ultimately culminating in a proof that the Yoneda embedding preserves limits.
Cardinality of Multisets
by Lukas Bulwahn
This entry provides three lemmas to count the number of multisets of a given size and finite carrier set. The first lemma provides a cardinality formula assuming that the multiset's elements are chosen from the given carrier set. The latter two lemmas provide formulas assuming that the multiset's elements also cover the given carrier set, i.e., each element of the carrier set occurs in the multiset at least once.
The proof of the first lemma uses the argument of the recurrence relation for counting multisets. The proof of the second lemma is straightforward, and the proof of the third lemma is easily obtained using the first cardinality lemma. A challenge for the formalization is the derivation of the required induction rule, which is a special combination of the induction rules for finite sets and natural numbers. The induction rule is derived by defining a suitable inductive predicate and transforming the predicate's induction rule.
Enjoy!
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 14:17):From: Gerwin.Klein@data61.csiro.au
There are two new entries available in the AFP:
Source Coding Theorem
by Quentin Hibon and Lawrence Paulson
This document contains a proof of the necessary condition on the code
rate of a source code, namely that this code rate is bounded by the
entropy of the source. This represents one half of Shannon's source
coding theorem, which is itself an equivalence.
https://www.isa-afp.org/entries/Source_Coding_Theorem.shtml
A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor
by Zhe Hou, David Sanan, Alwen Tiu, and Yang Liu
We formalise the SPARCv8 instruction set architecture (ISA) which is
used in processors such as LEON3. Our formalisation can be specialised
to any SPARCv8 CPU, here we use LEON3 as a running example. Our model
covers the operational semantics for all the instructions in the
integer unit of the SPARCv8 architecture and it supports Isabelle code
export, which effectively turns the Isabelle model into a SPARCv8 CPU
simulator. We prove the language-based non-interference property for
the LEON3 processor. Our model is based on deterministic monad, which
is a modified version of the non-deterministic monad from NICTA/l4v.
https://www.isa-afp.org/entries/SPARCv8.shtml
Enjoy!
Gerwin
Last updated: Nov 21 2024 at 12:39 UTC