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;