import-natural-spec

Importing Natural Language Specifications into VDM-SL

Read a Markdown requirements document and convert it to a VDM-SL formal specification through interactive dialogue. The key challenge is that natural language is inherently ambiguous — this skill systematically identifies and resolves those ambiguities rather than silently guessing.

MD形式の自然言語仕様をVDM-SL形式仕様に変換する。自然言語の曖昧さを対話的に解消しながら、 漏れのない形式仕様を構築する。

Why This Skill Exists

The define-contract skill builds VDM-SL from scratch through Q&A. The extract-spec skill extracts VDM-SL from existing source code.

This skill fills the gap between them: the user already has a written specification (requirements document, design doc, API spec, etc.) but it's in natural language, not code. Rather than starting from zero or from code, we start from the document and systematically formalize it.

Dialogue Flow

Step 1: Read and Parse the Document

Ask the user for the MD file path (or accept it from the conversation context).

Read the file and identify its structure:

• Headings → potential module/agent boundaries
• Bullet lists → requirements, constraints, rules
• Numbered lists → sequential operations, workflows
• Tables → data models, field definitions
• Code blocks → existing type definitions, API schemas, examples
• Bold/italic text → emphasis on important constraints

Produce a structural summary for the user:

📄 Document Analysis: requirements.md

Found:
  Sections:        5 (potential modules/agents)
  Requirements:    23 bullet points
  Data models:     2 tables
  Constraints:     7 explicitly stated
  Examples:        3 code blocks

Identified agents/modules:
  1. "User Management" (lines 5-45)
  2. "Order Processing" (lines 47-120)
  3. "Payment Gateway" (lines 122-180)

Present this to the user and confirm the scope before proceeding.

Step 2: Requirement Classification

For each requirement found in the document, classify it:

Category	VDM-SL Mapping	Example from document
Data definition	types	"A user has name, email, and role"
Constraint	inv	"Email must be unique"
Operation	operations / functions	"The system shall allow users to register"
Pre-condition	pre	"Only active users can place orders"
Post-condition	post	"After payment, order status becomes confirmed"
State	state	"The system maintains a list of all orders"
Business rule	Combination of inv + pre + post	"Users cannot order more than their credit limit"