Bart Massey

# A "Real-World" Example

Let's take a look at Problem 21 from the recent Advent Of Code.

What a mess!

• It's a specification, but it doesn't look easy to figure out what it is telling you to write.

• It has a lot of detail, which is important to the contest but maybe less important to writing a good general-purpose simulator.

• Is it even sound and complete? Who can tell?

# Starting To Specify AOC21

Let's start by figuring out what kind of sets we are dealing with here. What are the entities described in the specification?

[PLAYERS, ITEMS, ATTRIBUTES, KINDS]

Let's start by nailing down what we know about PLAYERS:

#PLAYERS = 2
pc in PLAYERS
npc in PLAYERS
npc =/= pc

Maybe we would have just been better off using a Z shorthand for this and for some of the others:

PLAYERS ::= pc | npc KINDS ::= weapon | armor | ring ATTRIBUTES ::= hp | ac | dam

# Specifying Items

This is where the item table goes, right? No. The item table is too complicated and somewhat irrelevant. Instead, we'll give functions that describe a piece of equipment, but crucially not say more:

| kind : ITEMS -> KINDS
| damage : ITEMS -> N
| resistance : ITEMS -> N
| cost : ITEMS -> N

We could (should?) use a state schema for each item, but they won't change throughout the game, so global functions are easier to work with.

# Dealing With Attributes: Player State Schema

A player state has an identity (who's who), currently values for attributes, and a set of equipment.

----Player---
| who : PLAYERS
| status : ATTRIBUTES -> N
| equipment : P ITEM
| eff_damage, eff_resistance : N
|------------
| item_count weapon equipment = 1
| item_count armor equipment <= 1
| item_count ring equipment <= 2
| eff_damage = status dmg + item_effects damage equipment
| eff_resistance = status ac + item_effects resistance equipment
-------------

There are restrictions on what can be equipped.

# Item Count

The number of items of a given kind in the given equipment is given by the number of mappings in the kind function.

| item_count : KINDS -> P ITEMS -> N
| ---
| item_count k es = # (es <| kind |> {k})

Note that this definition depends on the range restriction operators and on the idea that the kind function can be thought of as a set of tuples with its own cardinality.

# Item Effects

It's necessary to say what the effects of a player's equipment are on the player's capabilities. We use an inductive definition to add up equipment effects.

| item_effects : (ITEMS -> N) -> P ITEMS -> N |--- | item_effects property {} = 0 | item_effects property ({e} union es) = | property e + item_effects property es

# Setting Up For Combat

At any given time, there is an attacker and a defender.

----Combatants---
| attacker, defender : Player
|----------------
| attacker.who =/= defender.who
-----------------

A combat round will consist of an attack, then switching sides and attacking the other way.

# Combat Turn

To describe a combat turn, we describe what happens during the turn: the attacker damages the defender, taking the defenders resistance and the attacker's damage into account.

----Combat---
| Delta Combatants
| combat_damage, new_hp : N
|------------
| combat_damage = min 1 (attacker.eff_damage -
|                        defender.eff_resistance)
| new_hp = max 0 (defender.status hp - combat_damage)
| defender'.status = defender.status (+) {(hp, new_hp)}
| attacker'.who = attacker.who
| defender'.who = defender.who
-------------

Note that HP cannot go below zero: dead is dead. Note also that a defender with good defence cannot gain health from the attack of a bad attacker.

# Post-Combat

One of two things must hold after a combat turn: either the defender is dead, or it's time to switch sides.

----Death---
| Xi Combatants
|-----------
| defender.status hp = 0
------------

----Switch_Sides---
| Delta Combatants
|------------------
| defender.status hp > 0
| attacker' = defender
| defender' = attacker
-------------------

Combat_Round =^= Combat /\ (Death \/ Switch_Sides)

This last line isn't quite right...

# What's Left?

• We need to express the idea of a fight as a series of combat rounds ending in death. This can be done with a function whose input is an initial equipment list and whose output is the victor of the fight. This function can be specified with a recursive state schema.

• We need to express the actual problem presented to us: find the cost of a minimum-cost equipment configuration that allows the pc to beat an unequipped npc with given initial stats.

• We need to construct a starting schema for the fight from

• We will need to express the idea of taking the minimum cost over all (legal) equipment lists such that the pc wins.

• In a few weeks, this is homework.

# What Else?

• Should get the spec into a tool-ready notation.

• Should typecheck the spec.

• Should prove any important properties of the spec.

• Use the spec to guide coding

• Won't exactly translate everywhere
• But need to see (maybe prove) correspondence between the code and the spec

# Is All This Really Necessary?

Of course not.

• I solved this problem in about 1.5 hours in Haskell. I believe my solution to be correct. It worked on the contest input.

• This spec took me about 5 hours to write. It's not done yet.

• The stakes here are unbelievably small. Who cares?