Willem van den Ende
d3cc48c0f7
- Level value object (1..10, level-capped health) - Health value object (non-negative, pure sub/add) - Status discriminated union (alive | dead) - Character entity with private constructor and static factory - 9 fast-check properties covering creation invariants - Allium spec with entities, rules, and invariants
71 lines
1.4 KiB
Plaintext
71 lines
1.4 KiB
Plaintext
-- allium: 3
|
|
|
|
-- allium: character-creation
|
|
|
|
------------------------------------------------------------
|
|
-- Value Types
|
|
------------------------------------------------------------
|
|
|
|
type Health {
|
|
value: Integer
|
|
requires: value >= 0
|
|
}
|
|
|
|
type Level {
|
|
value: Integer
|
|
requires: value >= 1 and value <= 10
|
|
}
|
|
|
|
type Status {
|
|
alive | dead
|
|
}
|
|
|
|
------------------------------------------------------------
|
|
-- Entities
|
|
------------------------------------------------------------
|
|
|
|
entity Character {
|
|
name: String
|
|
health: Health
|
|
status: Status
|
|
level: Level
|
|
factions: Set<Faction>
|
|
}
|
|
|
|
------------------------------------------------------------
|
|
-- Rules
|
|
------------------------------------------------------------
|
|
|
|
rule CharacterCreation {
|
|
when: Character.create(name, level)
|
|
ensures: character.health.value = 1000
|
|
ensures: character.status = alive
|
|
ensures: character.level = level
|
|
ensures: character.factions = empty
|
|
}
|
|
|
|
rule HealthNonNegative {
|
|
for c in Characters:
|
|
c.health.value >= 0
|
|
}
|
|
|
|
rule StatusAliveImpliesHealthPositive {
|
|
for c in Characters:
|
|
c.status = alive implies c.health.value > 0
|
|
}
|
|
|
|
rule StatusDeadImpliesHealthZero {
|
|
for c in Characters:
|
|
c.status = dead implies c.health.value = 0
|
|
}
|
|
|
|
rule MaxLevel {
|
|
for c in Characters:
|
|
c.level.value <= 10
|
|
}
|
|
|
|
rule MinLevel {
|
|
for c in Characters:
|
|
c.level.value >= 1
|
|
}
|