Semantic notation for logical specifications

spec.log

Ledger
  Entries is sequence of Position and Operation

Position
  Shares is Number
  Average Share Cost is Number
  Gains is (Gross Gain, Net Gain) is (Number, Number)
  Tax is Number
  Total is Shares times Average Share Cost

Operation
  is Buy or Sell
  Shares is Number
  Share Cost is Number
  Total is Shares times Share Cost

Operations is sequence of Operation

Ledger for Operations and Position
  Entries is sequence of, Position is (last Position or Position) after Operation
                          Operation is Operation

Shares of Position after Operation
  is, if Operation is Buy
         then (Position Shares plus Operation Shares)
      if Operation is Sell
         then (Position Shares minus Operation Shares)

Average Share Cost of Position after Operation
  is, if Operation is Buy
         then (Position Total plus Operation Total) divided by (Position Shares plus Operation Shares)
      if Operation is Sell
         then (Position Average Share Cost)

Gains of Position after Operation
  Gross Gain is, if Operation is Buy
                    then Zero
                 if Operation is Sell
                    then (Operation Share Cost minus Position Average Share Cost) times Operation Shares
  Net Gain is Position Net Gain plus Gross Gain

Tax of Position after Operation and Gains
  is, if Operation is Sell
      and Operation Total is greater than some TAXATION THRESHOLD
      and Gross Gains is greater than Zero
      and Net Gains is greater than Zero
          then (Net Gains times some TAXATION FACTOR)
      else Zero