Introducing Test Scenarios in SmartPy.io

SmartPy.io
Oct 18 · 2 min read

Proving properties of smart contracts is of paramount importance and one of Tezos’ moto is about formally verifying its infrastructure and smart contracts.

We claim that formal verification is not the only tool to understand a smart contract and before formally proving properties, one should first perform unit-tests or scenario tests. It has a few very useful consequences: we may discover bugs, we may discover properties that we want to formally prove and, finally, it may also be the case that, for a given smart contract, we only need a few tests to be convinced of what it’s doing and do not need the full formal verification machinery.

From day one, SmartPy.io has used test scenarios for this very purpose.

This small document explains a new version of these test scenarios that brings new nice capabilities.

An example

We start by an example.

Here is a very simple example of a smart contract doing something pretty useless: it stores two values and provides an entry point that can change its first value (called myParameter1) as long as it is bounded by 123.

import smartpy as sp# A class of contracts
class MyContract(sp.Contract):
def __init__(self, myParameter1, myParameter2):
self.init(myParameter1 = myParameter1,
myParameter2 = myParameter2)
# An entry point, i.e., a message receiver
# (contracts react to messages)
@sp.entryPoint
def myEntryPoint(self, params):
sp.verify(self.data.myParameter1 <= 123)
self.data.myParameter1 += params

This can be tested by defining the following test and scenario in the same script.

@addTest(name = "First test")
def test():
# We define a test scenario, called scenario,
# together with some outputs and checks
scenario = sp.testScenario()
# We first define a contract and add it to the scenario
c1 = MyContract(12, 123)
scenario += c1
# And send messages to some entry points of c1
scenario += c1.myEntryPoint(12)
scenario += c1.myEntryPoint(13)
scenario += c1.myEntryPoint(14)
scenario += c1.myEntryPoint(50)
scenario += c1.myEntryPoint(50)
scenario += c1.myEntryPoint(50) ### This will be refused
# Finally, we check the final storage of c1
scenario.verify(c1.data.myParameter1 == 151)

This definition can be evaluated in-browser in SmartPy.io or out-of-browser with SmartPyBasic and both compute the scenario.

In SmartPy.io, the scenario is computed and then displayed as an html document.
With SmartPyBasic, this is first computed as a .json scenario file that is then evaluated.

Scenarios

As seen in the previous example, a scenario in a test is introduced by sp.testScenario(). We interact with it by using several constructions.

  • Registering and displaying contracts.
scenario += c1# This is identical to doing
scenario.register(c1, show = True)
# To only register the smart contract but not show it
scenario.register(c1)
  • Registering and displaying calls to entry points.
scenario += c1.myEntryPoint(12)
scenario += c1.myEntryPoint(...).run(sender = ..., amount = ..., now = ...)
# To only execute a call to an entry point but not show it
scenario.register(c1.myEntryPoint(12))
  • Adding document informations
scenario.h1("a title")
scenario.h2("a subtitle")
scenario.h3(..)
scenario.h4(..)
scenario.p("Some text")
  • Computing expressions.
scenario.compute(c1.data.myParameter1 * 12)
scenario.compute(c1.data)
  • Checking assertions.
scenario.verify(self.data.myParameter == 51)

SmartPy.io

Written by

An intuitive and effective smart contracts language and development platform for Tezos. In Python.

Welcome to a place where words matter. On Medium, smart voices and original ideas take center stage - with no ads in sight. Watch
Follow all the topics you care about, and we’ll deliver the best stories for you to your homepage and inbox. Explore
Get unlimited access to the best stories on Medium — and support writers while you’re at it. Just $5/month. Upgrade