This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// Data types to model the domain | |
type Key(==) // Keys support equality | |
type Flags | |
type Time = nat | |
type Data | |
datatype option<T> = | |
none | some(get: T) | |
datatype Entry |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
type Elem = int | |
/*** Specification ***/ | |
trait SpecSet { | |
ghost var content: set<Elem> | |
method insert(x: Elem) | |
modifies this | |
ensures content == old(content) + {x} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
theory Mergesort | |
imports Main | |
begin | |
fun sorted :: "nat list ⇒ bool" where | |
"sorted [] = True" | | |
"sorted (x#[]) = True" | | |
"sorted (x#y#zs) = (x ≤ y ∧ sorted (y#zs))" | |
fun merge :: "nat list ⇒ nat list ⇒ nat list" where |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* using tactics *) | |
lemma "A ∧ B ⟶ B ∧ A" | |
apply (rule impI) (* A ∧ B ⟹ B ∧ A *) | |
apply (rule conjI) (* 1: A ∧ B ⟹ B and 2: A ∧ B ⟹ A *) | |
(* goal 1 *) | |
apply (erule conjE) (* A ⟹ B ⟹ B *) | |
apply assumption | |
(* goal 2 *) | |
apply (erule conjE) (* A ⟹ B ⟹ A *) | |
apply assumption |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
class Expr: | |
def eval(self, state): | |
pass | |
class Var(Expr): | |
def __init__(self, name): | |
self.name = name | |
def eval(self, state): | |
return state[name] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
theory RegularBehavioralHoareLogic | |
imports Main | |
begin | |
(* Mechanization of | |
Gidon Ernst, Alexander Knapp, and Toby Murray: | |
A Hoare Logic with Regular Behavioral Specifications | |
submitted to ISoLa 2022 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
begin | |
fun mult :: "nat ⇒ nat ⇒ nat" where | |
"mult x 0 = 0" | | |
"mult x y = x + mult x (y - 1)" | |
lemma mult_rec[simp]: | |
"y ≠ 0 ⟹ mult x y = x + mult x (y - 1)" | |
by (cases y) auto |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(declare-datatypes ((Nat 0)) (((Z) (S (proj1-S Nat))))) | |
(declare-datatypes ((list 0)) | |
(((nil) (cons (head Nat) (tail list))))) | |
(define-fun-rec | |
== | |
((x Nat) (y Nat)) Bool | |
(match x | |
((Z | |
(match y | |
((Z true) |