From fc2cf73b343c69bc25d9b06d104c2cd63568de2d Mon Sep 17 00:00:00 2001 From: Willem van den Ende Date: Sat, 13 Jun 2026 15:28:34 +0100 Subject: [PATCH] =?UTF-8?q?feat:=20story=202=20=E2=80=94=20Characters=20ca?= =?UTF-8?q?n=20Deal=20Damage=20to=20Characters?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Allium spec: damage-and-health.allium - 5 fast-check properties: damage reduces health, health non-negative, death at zero, self-damage forbidden, dead cannot take damage - Character.createWithHealth factory for testing with arbitrary health - Character.dealDamage(target, damage) method --- specs/damage-and-health.allium | 49 +++++++++++++++ src/Character.ts | 52 +++++++++++++--- src/damage-and-health.spec.ts | 110 +++++++++++++++++++++++++++++++++ 3 files changed, 202 insertions(+), 9 deletions(-) create mode 100644 specs/damage-and-health.allium create mode 100644 src/damage-and-health.spec.ts diff --git a/specs/damage-and-health.allium b/specs/damage-and-health.allium new file mode 100644 index 0000000..f15b6f2 --- /dev/null +++ b/specs/damage-and-health.allium @@ -0,0 +1,49 @@ +-- allium: 3 + +-- allium: damage-and-health + +------------------------------------------------------------ +-- Rules +------------------------------------------------------------ + +rule DamageReducesHealth { + when: Character.dealDamage(attacker, target, damage) + requires: attacker.name != target.name + requires: target.status = alive + ensures: target.health.value = target.health.value - damage + ensures: + if target.health.value - damage <= 0: + target.status = dead + else: + target.status = alive +} + +rule SelfDamageForbidden { + when: Character.dealDamage(attacker, target, damage) + requires: attacker.name = target.name + ensures: + target.health.value = target.health.value + target.status = target.status +} + +rule DeadCannotTakeDamage { + when: Character.dealDamage(attacker, target, damage) + requires: target.status = dead + ensures: + target.health.value = target.health.value + target.status = dead +} + +------------------------------------------------------------ +-- Invariants +------------------------------------------------------------ + +invariant HealthNonNegative { + for c in Characters: + c.health.value >= 0 +} + +invariant DeathAtZeroHealth { + for c in Characters: + c.health.value = 0 implies c.status = dead +} diff --git a/src/Character.ts b/src/Character.ts index 6d7f540..6fd76dd 100644 --- a/src/Character.ts +++ b/src/Character.ts @@ -1,13 +1,13 @@ /** - * Character entity — immutable, value-object-driven. + * Character entity — value-object-driven. * - * "I can't believe it's not Haskell": no mutation, invariants at boundaries. + * "I can't believe it's not Haskell": invariants at boundaries. * State is encapsulated in a CharacterState record type. */ import { Health } from './Health.ts'; import type { Level } from './Level.ts'; import type { Status } from './Status.ts'; -import { StatusAlive } from './Status.ts'; +import { StatusAlive, StatusDead } from './Status.ts'; import { CharacterState } from './CharacterState.ts'; import type { Faction } from './Faction.ts'; @@ -16,8 +16,18 @@ export interface CharacterCtor { level: Level; } +export interface CharacterCtorWithHealth { + name: string; + level: Level; + health: number; +} + export class Character { - private constructor(readonly state: CharacterState) {} + #state: CharacterState; + + private constructor(state: CharacterState) { + this.#state = state; + } /** Create a new character with default health (1000) and alive status. */ static create({ name, level }: CharacterCtor): Character { @@ -25,23 +35,47 @@ export class Character { return new Character(state); } + /** Create a character with a specific health value (for testing). */ + static createWithHealth({ name, level, health }: CharacterCtorWithHealth): Character { + const state = new CharacterState(name, Health.create(health), StatusAlive, level, new Set()); + return new Character(state); + } + get name(): string { - return this.state.name; + return this.#state.name; } get health(): Health { - return this.state.health; + return this.#state.health; } get status(): Status { - return this.state.status; + return this.#state.status; } get level(): Level { - return this.state.level; + return this.#state.level; } get factions(): ReadonlySet { - return this.state.factions; + return this.#state.factions; + } + + /** Deal damage to another character. Mutates target in place. */ + dealDamage(target: Character, damage: number): void { + // Self-damage is forbidden + if (this.name === target.name) return; + // Dead characters cannot take damage + if (target.status.kind === 'dead') return; + // Reduce health + const newHealth = target.health.sub(damage); + const newStatus = newHealth.value === 0 ? StatusDead : StatusAlive; + target.#state = new CharacterState( + target.name, + newHealth, + newStatus, + target.level, + target.factions, + ); } } diff --git a/src/damage-and-health.spec.ts b/src/damage-and-health.spec.ts new file mode 100644 index 0000000..9990273 --- /dev/null +++ b/src/damage-and-health.spec.ts @@ -0,0 +1,110 @@ +import fc from 'fast-check'; +import { describe, it } from 'vitest'; +import { Character } from './Character.ts'; +import { Level } from './Level.ts'; + +describe('DamageAndHealth', () => { + describe('DamageReducesHealth', () => { + it('property: health is reduced by the damage amount', () => { + fc.assert( + fc.property( + fc.integer({ min: 0, max: 1000 }), + fc.integer({ min: 0, max: 10000 }), + (health, damage) => { + const attacker = Character.create({ name: 'attacker', level: Level.create(1) }); + const target = Character.createWithHealth({ + name: 'target', + level: Level.create(1), + health, + }); + const expected = Math.max(0, health - damage); + attacker.dealDamage(target, damage); + return target.health.value === expected; + }, + ), + ); + }); + }); + + describe('HealthNonNegative', () => { + it('property: health never goes below zero after damage', () => { + fc.assert( + fc.property( + fc.integer({ min: 0, max: 1000 }), + fc.integer({ min: 0, max: 10000 }), + (health, damage) => { + const attacker = Character.create({ name: 'attacker', level: Level.create(1) }); + const target = Character.createWithHealth({ + name: 'target', + level: Level.create(1), + health, + }); + attacker.dealDamage(target, damage); + return target.health.value >= 0; + }, + ), + ); + }); + }); + + describe('DeathAtZeroHealth', () => { + it('property: character dies when health reaches zero', () => { + fc.assert( + fc.property( + fc.integer({ min: 0, max: 1000 }), + fc.integer({ min: 0, max: 10000 }), + (health, damage) => { + const attacker = Character.create({ name: 'attacker', level: Level.create(1) }); + const target = Character.createWithHealth({ + name: 'target', + level: Level.create(1), + health, + }); + attacker.dealDamage(target, damage); + const expected = Math.max(0, health - damage); + if (expected === 0) { + return target.status.kind === 'dead'; + } + return target.status.kind === 'alive'; + }, + ), + ); + }); + }); + + describe('SelfDamageForbidden', () => { + it('property: a character cannot deal damage to itself — health unchanged', () => { + fc.assert( + fc.property( + fc.integer({ min: 0, max: 1000 }), + fc.integer({ min: 0, max: 10000 }), + (health, damage) => { + const c = Character.createWithHealth({ name: 'hero', level: Level.create(1), health }); + const healthBefore = c.health.value; + const statusBefore = c.status.kind; + c.dealDamage(c, damage); + return c.health.value === healthBefore && c.status.kind === statusBefore; + }, + ), + ); + }); + }); + + describe('DeadCannotTakeDamage', () => { + it('property: dead characters cannot take damage — state unchanged', () => { + fc.assert( + fc.property(fc.integer({ min: 0, max: 10000 }), (damage) => { + const attacker = Character.create({ name: 'attacker', level: Level.create(1) }); + const target = Character.create({ name: 'target', level: Level.create(1) }); + // Kill the target first + attacker.dealDamage(target, 10000); + const healthBefore = target.health.value; + const statusBefore = target.status.kind; + // Then try to deal more damage + attacker.dealDamage(target, damage); + return target.health.value === healthBefore && target.status.kind === statusBefore; + }), + ); + }); + }); +});