Modeling With Z

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?