#triplet #correctness A Hoare triple is a formal notation used to specify the [[correctness]] of a computer program or algorithm. It was introduced by British computer scientist [[Antony Hoare|Tony Hoare]] and is also known as [[Hoare triple|Hoare logic]] or [[Hoare triple|Hoare notation]], which can be simplified as [[source code + computation = output]]. **See [[Behavior-driven development#Hoare Triple and BDD]]**. In a Hoare triple, there are three parts: a [[precondition]], a [[command]], and a [[postcondition]]. The precondition describes the state of the program before executing the command, while the postcondition describes the expected state after executing the command. # Formal Definition of Hoare Triple The notation for a Hoare triple is $\{P\} C \{Q\}$, where $P$ represents the precondition, $C$ represents the command, and $Q$ represents the postcondition. $P$ and $Q$ are logical assertions that describe properties or conditions that hold true about variables or program states. ![[HoareTripleDiagram.png]] The precondition specifies what must be true before executing the command in order for it to start correctly. It typically includes initial values of variables and any necessary conditions for execution. The postcondition specifies what must be true after executing the command in order for it to terminate correctly. It describes any changes made to variables or program states due to the execution of the command. # Hoare Triple and the Lens Abstraction Dynamic systems may be modeled using the Hoare Triple and Lens abstractions, according to the Category Theory literature. The formal nomenclature In program verification, Hoare Triple defines preconditions, postconditions, and program behavior. $Q$ is the postcondition, while $P$ represents the precondition and $C$ the command or program. The transition of $C$ from satisfying $P$ to satisfying $Q$ is governed by the Hoare Triple. A Lens, on the other hand, is an abstraction of Category Theory that represents bidirectional transformations between structures. Typically, a lens comprises two operations: one, which retrieves a focused view from a given structure, and the other, which updates it. Lenses enable the modification and observation of structures while preserving referential transparency. State transitions and input-output interactions are focal points of both concepts. By analyzing how operations or transformations convert input states to output states, the Hoare Triple and Lens are utilized. By designating program or instruction preconditions (input states) and postconditions (output states), Hoare Triple models this transition. It ensures that invoking a program with specific preconditions results in the fulfillment of particular postconditions. Lens utilizes setters to update particular components of a structure (output state) and getters to concentrate on those components (input state). The lens monitors changes and permits bidirectional state transformations. In comparison to the input/output modeling of the Hoare Triple, Lens's representation of dynamical systems is critical. Both methodologies prioritize the comprehension of how states evolve over time or as a result of actions. Lens is a dynamical system abstraction that simulates the behavior of the system as its state changes. The lens symbolizes the correlation among phases within a dynamical system, similar to the Hoare The input and output states of a program are denoted by Triple. In general, the Hoare Triple and Lens models represent interactions between inputs and outputs. Lens is concerned with bidirectional transformations of data structures, whereas Hoare Triple is concerned with preconditions, postconditions, and commands for program verification. Both approaches aid comprehension of system evolution. # Explained by Hoare Himself ![[@turingawardeeclipsHoareDefinitionPurpose2020|Hoare on the definition and purpose of the Hoare Triple]] Hoare triples are used in formal verification techniques such as program proving and model checking. They provide a way to reason about program [[correctness]] by mathematically specifying desired properties and verifying if those properties hold true after program execution. By using Hoare triples, programmers can formally reason about their programs' behavior, ensure [[correctness]], and detect potential bugs or errors early in development. They also aid in designing test cases that cover all possible scenarios according to specified [[precondition|preconditions]] and [[postcondition|postconditions]]. Overall, Hoare triples provide a powerful method for specifying and verifying program correctness using logical assertions before and after executing commands. # References ```dataview Table title as Title, authors as Authors where contains(subject, "Hoare Triple") or contains(subject, "source code + computation = output") ``` ![[@ethereumengineeringgroupEth2SpecsFormal2020|Eth2.0 specs: formal verification using Dafny]]