This Is Boogie 2

Leino, K. R. M. (2008). This Is Boogie 2.

Type

Report

Intellectual base

Grey literature

Year

2008

Link

https://www.microsoft.com/en-us/research/publication/this-is-boogie-2-2/

Cited from

philosophy

Cited by

1 citation across 1 artifact.

Each citation links to the sentence it supports in the citing article.

Primes

• Epistemic Mode Of A Proposition
  • In programming and formal methods, the modes are explicit in the language: an assert checks a proposition that should hold and halts if it does not, an assume (in verification) is relied on without checking, an invariant is a proposition required to hold at every iteration, a precondition is a premise the caller must discharge, and a postcondition is an asserted guarantee — and a verification tool's soundness depends on never confusing an assume (taken on trust) with an assert (checked).

    This sourceSpecifies the verification language's assert (an expression required to hold in every correct trace — checked) versus assume (an expression taken to hold in every feasible trace — relied on without checking), with preconditions/postconditions — supporting the assert/assume/precondition modes, that soundness depends on not confusing assume with assert, and the catastrophic mode error of writing assume where assert was required.

Verification

This reference passed the adversarial substantiation pipeline: it was checked to exist and to support the claim it is attached to. See how references were verified.

Registry ID ref:c18f055364ea · see in the full table