Compare commits
2
Commits
39839dc594
..
main
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
21bd58be33 | ||
|
|
31984bbd9d |
@@ -1,174 +0,0 @@
|
|||||||
-- allium: 3
|
|
||||||
|
|
||||||
-- allium: magical-objects
|
|
||||||
|
|
||||||
------------------------------------------------------------
|
|
||||||
-- External Entities
|
|
||||||
------------------------------------------------------------
|
|
||||||
|
|
||||||
external entity Character {
|
|
||||||
name: String
|
|
||||||
health: Health
|
|
||||||
status: alive | dead
|
|
||||||
level: Level
|
|
||||||
factions: Set<Faction>
|
|
||||||
}
|
|
||||||
|
|
||||||
external entity Health {
|
|
||||||
value: Integer
|
|
||||||
}
|
|
||||||
|
|
||||||
external entity Level {
|
|
||||||
value: Integer
|
|
||||||
}
|
|
||||||
|
|
||||||
external entity Faction {
|
|
||||||
name: String
|
|
||||||
}
|
|
||||||
|
|
||||||
------------------------------------------------------------
|
|
||||||
-- Entities and Variants
|
|
||||||
------------------------------------------------------------
|
|
||||||
|
|
||||||
entity MagicalWeapon {
|
|
||||||
health: Health
|
|
||||||
maxHealth: Integer
|
|
||||||
status: alive | destroyed
|
|
||||||
damage: Integer
|
|
||||||
owner: Character
|
|
||||||
}
|
|
||||||
|
|
||||||
entity HealingObject {
|
|
||||||
health: Health
|
|
||||||
maxHealth: Integer
|
|
||||||
status: alive | destroyed
|
|
||||||
}
|
|
||||||
|
|
||||||
------------------------------------------------------------
|
|
||||||
-- Rules
|
|
||||||
------------------------------------------------------------
|
|
||||||
|
|
||||||
rule WeaponDealsDamage {
|
|
||||||
when: MagicalWeapon.dealsDamage(weapon, target, attacker)
|
|
||||||
requires: weapon.status = alive
|
|
||||||
requires: attacker = weapon.owner
|
|
||||||
requires: attacker.status = alive
|
|
||||||
ensures: target.health.value = max(0, target.health.value - weapon.damage)
|
|
||||||
ensures: weapon.health.value = weapon.health.value - 1
|
|
||||||
ensures:
|
|
||||||
if weapon.health.value - 1 = 0:
|
|
||||||
weapon.status = destroyed
|
|
||||||
else:
|
|
||||||
weapon.status = alive
|
|
||||||
ensures:
|
|
||||||
if max(0, target.health.value - weapon.damage) = 0:
|
|
||||||
target.status = dead
|
|
||||||
else:
|
|
||||||
target.status = alive
|
|
||||||
}
|
|
||||||
|
|
||||||
rule DeadCannotUseWeapon {
|
|
||||||
when: MagicalWeapon.dealsDamage(weapon, target, attacker)
|
|
||||||
requires: attacker.status = dead
|
|
||||||
ensures:
|
|
||||||
target.health.value = target.health.value
|
|
||||||
weapon.health.value = weapon.health.value
|
|
||||||
weapon.status = weapon.status
|
|
||||||
target.status = target.status
|
|
||||||
}
|
|
||||||
|
|
||||||
rule NonOwnerCannotUseWeapon {
|
|
||||||
when: MagicalWeapon.dealsDamage(weapon, target, attacker)
|
|
||||||
requires: attacker != weapon.owner
|
|
||||||
ensures:
|
|
||||||
target.health.value = target.health.value
|
|
||||||
weapon.health.value = weapon.health.value
|
|
||||||
weapon.status = weapon.status
|
|
||||||
target.status = target.status
|
|
||||||
}
|
|
||||||
|
|
||||||
rule DestroyedWeaponCannotDealDamage {
|
|
||||||
when: MagicalWeapon.dealsDamage(weapon, target, attacker)
|
|
||||||
requires: weapon.status = destroyed
|
|
||||||
ensures:
|
|
||||||
target.health.value = target.health.value
|
|
||||||
weapon.health.value = weapon.health.value
|
|
||||||
weapon.status = weapon.status
|
|
||||||
target.status = target.status
|
|
||||||
}
|
|
||||||
|
|
||||||
rule HealingObjectHealsCharacter {
|
|
||||||
when: HealingObject.healsCharacter(object, character, amount)
|
|
||||||
requires: object.status = alive
|
|
||||||
requires: character.status = alive
|
|
||||||
ensures: healAmount = min(amount, object.maxHealth - object.health.value)
|
|
||||||
ensures: character.health.value = character.health.value + healAmount
|
|
||||||
ensures: object.health.value = object.health.value - healAmount
|
|
||||||
ensures:
|
|
||||||
if object.health.value - healAmount = 0:
|
|
||||||
object.status = destroyed
|
|
||||||
else:
|
|
||||||
object.status = alive
|
|
||||||
}
|
|
||||||
|
|
||||||
rule DeadCannotUseHealingObject {
|
|
||||||
when: HealingObject.healsCharacter(object, character, amount)
|
|
||||||
requires: character.status = dead
|
|
||||||
ensures:
|
|
||||||
character.health.value = character.health.value
|
|
||||||
object.health.value = object.health.value
|
|
||||||
object.status = object.status
|
|
||||||
}
|
|
||||||
|
|
||||||
rule DestroyedHealingObjectCannotHeal {
|
|
||||||
when: HealingObject.healsCharacter(object, character, amount)
|
|
||||||
requires: object.status = destroyed
|
|
||||||
ensures:
|
|
||||||
character.health.value = character.health.value
|
|
||||||
object.health.value = object.health.value
|
|
||||||
object.status = object.status
|
|
||||||
}
|
|
||||||
|
|
||||||
------------------------------------------------------------
|
|
||||||
-- Invariants
|
|
||||||
------------------------------------------------------------
|
|
||||||
|
|
||||||
invariant WeaponHealthNeverNegative {
|
|
||||||
for w in MagicalWeapons:
|
|
||||||
w.health.value >= 0
|
|
||||||
}
|
|
||||||
|
|
||||||
invariant WeaponDestroyedAtZeroHealth {
|
|
||||||
for w in MagicalWeapons:
|
|
||||||
w.health.value = 0 implies w.status = destroyed
|
|
||||||
}
|
|
||||||
|
|
||||||
invariant WeaponMaxHealthNeverExceeded {
|
|
||||||
for w in MagicalWeapons:
|
|
||||||
w.health.value <= w.maxHealth
|
|
||||||
}
|
|
||||||
|
|
||||||
invariant HealingObjectHealthNeverNegative {
|
|
||||||
for h in HealingObjects:
|
|
||||||
h.health.value >= 0
|
|
||||||
}
|
|
||||||
|
|
||||||
invariant HealingObjectDestroyedAtZeroHealth {
|
|
||||||
for h in HealingObjects:
|
|
||||||
h.health.value = 0 implies h.status = destroyed
|
|
||||||
}
|
|
||||||
|
|
||||||
invariant HealingObjectMaxHealthNeverExceeded {
|
|
||||||
for h in HealingObjects:
|
|
||||||
h.health.value <= h.maxHealth
|
|
||||||
}
|
|
||||||
|
|
||||||
invariant HealingObjectCannotDealDamage {
|
|
||||||
for h in HealingObjects:
|
|
||||||
not h.dealsDamage(_, _)
|
|
||||||
}
|
|
||||||
|
|
||||||
invariant WeaponCannotHeal {
|
|
||||||
for w in MagicalWeapons:
|
|
||||||
not w.healsCharacter(_, _)
|
|
||||||
}
|
|
||||||
@@ -16,7 +16,7 @@ An implementation of the RPG Combat rules engine. There are six user stories des
|
|||||||
|
|
||||||
This project combines three practices:
|
This project combines three practices:
|
||||||
|
|
||||||
1. **Allium** (`.allium` specs) — formal behavioural specifications that capture _what_ the system does
|
1. **Allium** (`.allium` specs) — formal behavioural specifications that capture _what_ the system does. All specs live in [specs/](specs/) — one file per story/domain area.
|
||||||
2. **fast-check** — property-based testing that verifies those properties hold across thousands of random inputs
|
2. **fast-check** — property-based testing that verifies those properties hold across thousands of random inputs
|
||||||
3. **"I can't believe it's not Haskell"** — TypeScript with ADTs, value objects, and immutability
|
3. **"I can't believe it's not Haskell"** — TypeScript with ADTs, value objects, and immutability
|
||||||
|
|
||||||
|
|||||||
@@ -85,7 +85,9 @@ Two custom extensions were developed for this project:
|
|||||||
|
|
||||||
### The Transcript Archive
|
### The Transcript Archive
|
||||||
|
|
||||||
Every session is exported as an HTML transcript in the `transcripts/` directory — over 20 sessions documenting the full journey from first requirements review through horizontal refactoring. These are the project's most valuable artifacts.
|
Every session is exported as an HTML transcript in the `transcripts/` directory — 28 sessions documenting the full journey from first requirements review through horizontal refactoring. See the [full transcript index](transcripts/index.md) for a chronological list.
|
||||||
|
|
||||||
|
These are the project's most valuable artifacts.
|
||||||
|
|
||||||
## Build & Test
|
## Build & Test
|
||||||
|
|
||||||
|
|||||||
@@ -136,6 +136,8 @@ rule DeadCannotUseWeapon {
|
|||||||
ensures:
|
ensures:
|
||||||
target.health.value = target.health.value
|
target.health.value = target.health.value
|
||||||
weapon.health.value = weapon.health.value
|
weapon.health.value = weapon.health.value
|
||||||
|
weapon.status = weapon.status
|
||||||
|
target.status = target.status
|
||||||
}
|
}
|
||||||
|
|
||||||
rule NonOwnerCannotUseWeapon {
|
rule NonOwnerCannotUseWeapon {
|
||||||
@@ -146,6 +148,8 @@ rule NonOwnerCannotUseWeapon {
|
|||||||
ensures:
|
ensures:
|
||||||
target.health.value = target.health.value
|
target.health.value = target.health.value
|
||||||
weapon.health.value = weapon.health.value
|
weapon.health.value = weapon.health.value
|
||||||
|
weapon.status = weapon.status
|
||||||
|
target.status = target.status
|
||||||
}
|
}
|
||||||
|
|
||||||
rule WeaponDestroyedCannotDealDamage {
|
rule WeaponDestroyedCannotDealDamage {
|
||||||
@@ -156,6 +160,8 @@ rule WeaponDestroyedCannotDealDamage {
|
|||||||
ensures:
|
ensures:
|
||||||
target.health.value = target.health.value
|
target.health.value = target.health.value
|
||||||
weapon.health.value = weapon.health.value
|
weapon.health.value = weapon.health.value
|
||||||
|
weapon.status = weapon.status
|
||||||
|
target.status = target.status
|
||||||
}
|
}
|
||||||
|
|
||||||
------------------------------------------------------------
|
------------------------------------------------------------
|
||||||
|
|||||||
@@ -0,0 +1,34 @@
|
|||||||
|
# Transcript Archive
|
||||||
|
|
||||||
|
Chronological list of all session transcripts from the RPG Combat project.
|
||||||
|
|
||||||
|
| Date | Transcript |
|
||||||
|
| ---- | ---------- |
|
||||||
|
| 2026-06-12 20:20 | [Card, Conversation & Confirmation](card-conversation-confirmation.html) |
|
||||||
|
| 2026-06-12 20:20 | [Install Allium](install-allium.html) |
|
||||||
|
| 2026-06-12 20:20 | [Review User Stories](review-user-stories.md) |
|
||||||
|
| 2026-06-12 23:02 | [Clear and Export](clear-and-export.html) |
|
||||||
|
| 2026-06-12 23:02 | [Refactor Story 1](refactor-story-1.html) |
|
||||||
|
| 2026-06-12 23:02 | [Story 1 — Process Improvement](story1-process-improvement.md) |
|
||||||
|
| 2026-06-13 15:42 | [YAGNI in AGENTS.md](yagni-in-agents-md.html) |
|
||||||
|
| 2026-06-13 15:51 | [Story 2 — Refactored](story-2-refactored.html) |
|
||||||
|
| 2026-06-13 16:06 | [Forgot to Mention the Story](forgot-to-mention-the-story.html) |
|
||||||
|
| 2026-06-13 22:03 | [Forgot to Commit](forgot-to-commit.html) |
|
||||||
|
| 2026-06-13 22:03 | [Story 2 (re?) — Done](story-2-(re?)-done.html) |
|
||||||
|
| 2026-06-13 22:20 | [Story 4 — Built](story-4-built.html) |
|
||||||
|
| 2026-06-13 22:32 | [Found Out Story 3 Is Not Done](found-out-story-3-is-not-done.html) |
|
||||||
|
| 2026-06-14 10:48 | [Break Down Horizontal Refactoring into Yaks](break-down-horizontal-refactoring-into-yaks.html) |
|
||||||
|
| 2026-06-14 10:48 | [Create Task Breakdown with Yaks Skill](create-task-breakdown-with-yaks-skill.html) |
|
||||||
|
| 2026-06-14 10:48 | [Fixed Character Implementation (Maybe)](fixed-character-implementation-maybe.html) |
|
||||||
|
| 2026-06-14 10:51 | [Resolved Circular Dependency](resolved-circular-dependency.html) |
|
||||||
|
| 2026-06-14 12:01 | [Break Down the Refactoring Yaks](break-down-the-refactoring-yaks.html) |
|
||||||
|
| 2026-06-14 12:01 | [Break Yaks Down into Phases](break-yaks-down-into-phases.html) |
|
||||||
|
| 2026-06-14 12:01 | [Yaks Were Not Marked S-Done](yaks-were-not-marked-s-done.html) |
|
||||||
|
| 2026-06-14 12:47 | [Create Yak Run Skill](create-yak-run-skill.html) |
|
||||||
|
| 2026-06-14 12:47 | [ESLint Rule Against Value Objects and Yaks to Refactor](eslint-rule-against-value-objects-and-yaks-to-refactor.html) |
|
||||||
|
| 2026-06-14 12:47 | [Generate README](generate-readme.html) |
|
||||||
|
| 2026-06-14 12:47 | [Yaks Work for Horizontal Refactoring](yaks-work-for-horizontal-refactoring.html) |
|
||||||
|
| 2026-06-14 14:26 | [Refactor: Replace Number Health with Health Value Object in MagicalObject](refactor:-replace-number-health-with-Health-value-object-in-MagicalObject.html) |
|
||||||
|
| 2026-06-14 14:26 | [Story 4 Also Done — Spec and Story Needed to Be Put Straight](story-4-also-done,-spec-and-story-needed-to-be-put-straight.html) |
|
||||||
|
| 2026-06-15 08:09 | [Last Story Done](last-story-done.html) |
|
||||||
|
| 2026-06-15 09:36 | [Wrap Up](wrap-up.html) |
|
||||||
File diff suppressed because one or more lines are too long
File diff suppressed because one or more lines are too long
Reference in New Issue
Block a user