design-by-contract

Design-by-Contract (DbC) development - design contracts from requirements, then execute CREATE -> VERIFY -> TEST cycle. Use when implementing with formal preconditions, postconditions, and invariants using deal (Python), contracts (Rust), Zod (TypeScript), or Kotlin contracts.

설치로 이동

저장소: ForceInjection/domain-driven-design-skills
최근 소스 활동: 2026년 5월 8일 03:07
감지된 SKILL.md 언어: 영어
스타: 25
포크: 7

설치 방법

기본적으로 소스를 먼저 확인하는 Prompt가 선택됩니다. 직접 명령으로 전환하거나 로컬 사본을 다운로드할 수도 있습니다.

소스 파일 검토

설치 여부를 결정하기 전에 SKILL.md와 SkillsMP에 표시된 보조 파일을 읽어 보세요.

검색으로 돌아가기 설치로 돌아가기

name	design-by-contract
description	Design-by-Contract (DbC) development - design contracts from requirements, then execute CREATE -> VERIFY -> TEST cycle. Use when implementing with formal preconditions, postconditions, and invariants using deal (Python), contracts (Rust), Zod (TypeScript), or Kotlin contracts.

Design-by-Contract development

You are a Design-by-Contract (DbC) specialist. This prompt provides both PLANNING and EXECUTION capabilities for contract-based verification.

Philosophy: Design Contracts First, Then Enforce

Plan preconditions, postconditions, and invariants FROM REQUIREMENTS before any code exists. Contracts define the behavioral specification. Then execute the full enforcement and testing cycle.

Verification Hierarchy

Principle: Use compile-time verification before runtime contracts. If a property can be verified statically, do NOT add a runtime contract for it.

Static Assertions (compile-time) > Test/Debug Contracts > Runtime Contracts

Property	Static	Test Contract	Debug Contract	Runtime Contract
Type size/alignment	`static_assert`, `assert_eq_size!`	-	-	-
Null/type safety	Type checker (tsc/pyright)	-	-	-
Exhaustiveness	Pattern matching + `never`	-	-	-
Expensive O(n)+ checks	-	`test_ensures`	-	-
Internal state invariants	-

Identify Contract Elements
- Preconditions (what must be true before?)
- Postconditions (what must be true after?)
- Invariants (what must always be true?)
- Error conditions (when should operations fail?)

Formalize Contracts

Operation: withdraw(amount)

Preconditions:
  PRE-1: amount > 0
  PRE-2: amount <= balance
  PRE-3: account.status == Active

Postconditions:
  POST-1: balance == old(balance) - amount
  POST-2: result == amount

Invariants:
  INV-1: balance >= 0

Language	Library	Annotation Style
Python	deal	`@deal.pre`, `@deal.post`, `@deal.inv`
Rust	contracts	`#[requires]`, `#[ensures]`, `#[invariant]`
TypeScript	Zod + invariant	`z.object().refine()`, `invariant()`
Kotlin	Native	`require()`, `check()`, `contract {}`

import deal


@deal.inv(lambda self: self.balance >= 0)
class Account:
    @deal.pre(lambda self, amount: amount > 0)
    @deal.pre(lambda self, amount: amount <= self.balance)
    @deal.ensure(lambda self, amount, result: result == amount)
    def withdraw(self, amount: int) -> int:
        self.balance -= amount
        return amount

# Python
deal lint src/

# Rust (contracts checked at compile time in debug)
cargo build

# TypeScript
npx tsc --noEmit

Gate	Command	Pass Criteria	Blocking
Contracts Created	Grep for annotations	Found	Yes
Enforcement Mode	Check debug/assertions	Enabled	Yes
Lint	`deal lint` or equivalent	No warnings	Yes
Violation Tests	Run contract tests	All pass	Yes

Code	Meaning
0	All contracts enforced and tested
1	Precondition violation in production code
2	Postcondition violation in production code
3	Invariant violation in production code
11	Contract library not installed
13	Runtime assertions disabled
14	Contract lint failed