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種別の詳細解説