Skip to content

Instantly share code, notes, and snippets.

@itsN1X

itsN1X/8216_spec_0xFFF.k

Forked from marekkirejczyk/spec.k
Last active March 20, 2019 20:38
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save itsN1X/95914538065d99872cd6c05b27fe4c2c to your computer and use it in GitHub Desktop.
Save itsN1X/95914538065d99872cd6c05b27fe4c2c to your computer and use it in GitHub Desktop.
Download ZIP
klab/examples/token/src/spec.md
Raw
8216_spec_0xFFF.k
behaviour transfer of Token
interface transfer(address To, uint Value)
types
FromBal : uint256
ToBal : uint256
storage
#Token.balances[CALLER_ID] |-> FromBal => FromBal - Value
#Token.balances[To] |-> ToBal => ToBal + Value
iff in range uint256
FromBal - Value
ToBal + Value
if
CALLER_ID =/= To
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment