Tag
specification
- Aug 27, 2026 What a Sandbox Proof Establishes and What It Assumes How verification of a sandbox reduces the isolation guarantee to a set of machine-checked lemmas, where the specification gap appears, and why the assumptions are the part that matters. language runtimes
- Aug 26, 2026 Exhaustive State Exploration and What a Bounded Model Proves How model checking enumerates reachable states, why a bound is a parameter of the claim rather than a shortcut, and how to read a counterexample as a requirement defect. software engineering
- Jan 10, 2026 Liveness and Fairness in Temporal Specifications Why safety properties need only one bad state to fail while liveness needs an infinite execution, and how a fairness assumption turns a starving scheduler into a specification bug. software engineering
- Aug 23, 2025 Refinement: When an Implementation Satisfies a Specification How refinement relates an abstract specification to concrete behaviour, why stuttering steps and history variables make the relation provable, and where refinement forbids implementation freedom. software engineering
- Jul 28, 2025 Inductive Invariants Over Reachable States Why an invariant that holds initially and is preserved by every step still needs an induction hypothesis, and how the strengthening problem makes proofs fail. software engineering
- Jun 17, 2025 Specifying Partial Failure, Atomicity, and Retry Semantics How a contract states what survives a crash mid-operation, why idempotency keys must be chosen by the caller, and where at-least-once delivery forces deduplication. software engineering
- Jun 15, 2024 Decision Tables and Rule Completeness in Policy Specifications How a decision table exposes overlapping and missing rules in eligibility logic, why hit policies change behaviour, and what completeness costs as conditions multiply. software engineering
- Mar 26, 2024 Specifying Behaviour as a State Machine with Guards Why a transition table beats prose for event-driven behaviour, how guards resolve overlapping transitions, and what unreachable states reveal about a specification. software engineering
- Nov 8, 2023 The Equivalence Relation That Refactoring Depends On Refactoring is defined as behavior-preserving change, which first requires deciding what counts as behavior. That decision is the whole discipline. software engineering
- Sep 18, 2023 Quantifier Scope and Undefined Terms in Requirement Statements Why "all users can see their orders" admits several incompatible readings, how scope ambiguity survives review, and what a rewrite into explicit quantifiers costs. software engineering
- May 31, 2023 Preconditions and Postconditions as the Function Contract How a function contract divides obligations between caller and implementer, what a runtime check costs, and where frame conditions and aliasing break the guarantee. software engineering
- May 18, 2023 Conformance Testing from a Specification: Distinguishing Sequences How a finite-state specification yields a test suite with a completeness argument, why a distinguishing sequence is necessary, and what the method assumes about the implementation. software engineering