kotaroyamame/formal-methods-guide

Formal Methods Guide

Answer questions about formal methods and VDM-SL in developer-friendly language. Always accompany technical terminology with plain explanations.

形式手法やVDM-SLに関する質問に、開発者が理解しやすい言葉で説明する。 専門用語を使う場合は必ず平易な説明を添える。

Three Pillars of Formal Methods

Formal methods are broadly divided into three areas:

形式手法は大きく3つの分野に分かれる:

1. Formal Specification (形式的仕様記述) — Mathematically describe system behavior (VDM-SL, TLA+, B-Method, Z)
2. Model Checking (モデル検査) — Exhaustively explore state spaces to verify properties (SPIN, NuSMV, TLA+)
3. Theorem Proving (定理証明) — Prove properties through logical reasoning (Coq, Isabelle/HOL, Lean)

This plugin focuses on Formal Specification, specifically VDM-SL.

本プラグインは形式的仕様記述、特にVDM-SLを中心に扱う。

VDM-SL Core Concepts

Types

The VDM-SL type system is the foundation for rigorously defining "what is exchanged" in inter-agent contracts.

VDM-SLの型システムは、エージェント間の契約で「何を受け渡すか」を厳密に定義する基盤。

Basic types:

• nat — natural numbers ≥ 0, nat1 — natural numbers ≥ 1
• int — integers, real — real numbers
• bool — boolean, char — character, token — abstract token

Compound types:

• seq of T — sequence (list) of T, seq1 of T — non-empty sequence
• set of T — set of T
• map K to V — map from K to V (dictionary)
• Record type — T :: field1 : Type1 field2 : Type2 defines a struct

Invariants (不変条件)

Declare conditions that "must always hold" for a type or state.

型や状態に対して「常に成り立つべき条件」を宣言する。

types
  Age = nat
  inv a == a <= 150;

This means "age must be between 0 and 150". This constraint is automatically included in verification targets wherever the type is used.

「年齢は0以上150以下」という制約。型を使うすべての箇所で自動的に検証対象になる。

Pre-conditions and Post-conditions (事前条件と事後条件)

Define "caller's responsibility" and "implementation's guarantee" for functions and operations.

関数や操作に対して「呼び出し側の責任」と「実装側の保証」を定義する。

functions
  divide: real * real -> real
  divide(a, b) == a / b
  pre b <> 0
  post RESULT * b = a;

• pre — condition the caller must satisfy (b is not zero)
• post — condition the result must satisfy (result × b = a)

State (状態)

Define mutable state that operations read and write.

操作が読み書きする可変状態を定義する。

state SystemState of
  users : map UserId to User
  nextId : UserId
inv mk_SystemState(users, nextId) == nextId not in set dom users
init s == s = mk_SystemState({|->}, 1)
end

Proof Obligation (PO) Types (証明責務の種類)

Major PO types generated by VDMJ with developer-friendly explanations:

VDMJが生成する主要なPO種別と開発者向けの平易な説明:

| PO Type | Japanese | Meaning | Developer Explanation | |---------|----------|---------|----------------------| | subtype | 部分型義務 | Value conforms to type constraints | "Does this value really fit this type?" | | invariant satisfiability | 不変条件充足 | A value satisfying the constraint can exist | "Is this constraint so strict that nothing can satisfy it?" | | map apply | 写像適用義務 | Key exists in the map | "Is it guaranteed we can look up this key?" | | total function | 全域関数義務 | Pre/post/invariant conditions evaluate correctly | "Can this condition itself cause an error?" | | func post condition | 関数事後条件 | Function satisfies its post-condition | "Does this function return what it promised?" | | operation postcondition | 操作事後条件 | Operation satisfies its post-condition | "Does this operation change state as promised?" | | state invariant | 状態不変条件 | State invariant maintained after operation | "Is system consistency preserved after the operation?" | | map compatible | 写像互換性 | Duplicate key values match when merging maps | "When merging two maps, do same keys have different values?" |

Role of Formal Methods in Multi-Agent Development

Formally defining inter-agent contracts provides:

エージェント間の契約を形式的に定義することで:

1. Eliminate ambiguity (曖昧さの排除) — Instead of "returns user info", explicitly specify types, constraints, and conditions
2. Automated verification (自動検証) — Detect contract violations before execution (PO generation → verification)
3. Clear responsibilities (責任の明確化) — Pre-condition = caller's responsibility, Post-condition = implementation's guarantee
4. Stepwise refinement (段階的詳細化) — From abstract spec to concrete implementation, ensuring consistency at each stage

Detailed References

For more detailed information, see the references/ directory:

より詳しい内容は references/ ディレクトリを参照:

• references/vdm-sl-syntax.md — Complete VDM-SL syntax reference / VDM-SL構文リファレンス
• references/po-types-detail.md — Detailed explanation of all PO types / PO種別の詳細解説