From dd97e0a58b377161fb8e9ab7b5524f63b875612c Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sat, 19 Mar 2022 17:26:39 +0000 Subject: Add definition of Hoare logic semantics. --- Everything.agda | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'Everything.agda') diff --git a/Everything.agda b/Everything.agda index aa36309..d547bcd 100644 --- a/Everything.agda +++ b/Everything.agda @@ -51,6 +51,12 @@ import Helium.Algebra.Structures -- Definition of the Armv8-M pseudocode. import Helium.Data.Pseudocode.Core +-- Ways to modify pseudocode statements and expressions. +import Helium.Data.Pseudocode.Manipulate + +-- Basic properties of the pseudocode data types +import Helium.Data.Pseudocode.Properties + -- Definition of types and operations used by the Armv8-M pseudocode. import Helium.Data.Pseudocode.Types @@ -63,5 +69,17 @@ import Helium.Instructions.Core -- Implementation of Barrett reduction. import Helium.Instructions.Instances.Barrett +-- Definition of assertions used in correctness triples +import Helium.Semantics.Axiomatic.Assertion + +-- Base definitions for the axiomatic semantics +import Helium.Semantics.Axiomatic.Core + +-- Definition of terms for use in assertions +import Helium.Semantics.Axiomatic.Term + +-- Definition of Hoare triples +import Helium.Semantics.Axiomatic.Triple + -- Base definitions for the denotational semantics. import Helium.Semantics.Denotational.Core -- cgit v1.2.3