Coder Social home page Coder Social logo

pyvdmc's Introduction

pyVDMC

pyVDMC is a VDMPad client library to animate VDM-SL specifications.

VDMC object

  >>> from pyVDMC import VDMC
  >>> vdm = VDMC()
  >>> vdm("1+2")
  u'3'

or with a specification,

  >>> from pyVDMC import VDMC
  >>> fib = VDMC("""
  /* fibonacci generator */
  state State of 
    n1 : nat 
    n2 : nat 
    init s == s = mk_State(0, 1)
  end 
  operations 
    next : () ==> nat 
    next() == (dcl n : nat := n1 + n2; n1 := n2; n2 := n; return n);
  """)
  >>> fib("next()")
  u'1'
  >>> fib("next()")
  u'2'
  >>> fib("next()")
  u'3'
  >>> fib("next()")
  u'5'
  >>> fib("next()")
  u'8'
  >>> fib("next()")
  u'13'
  >>> fib("next()")
  u'21'

DocString and Decorators

Decorators are also available. (Because we haven't developed value mappers, only values whose expressions can be interpreted in both VDM-SL and python is supported. Such values include numbers and lists.)

Here is another fibonacci example.

from pyVDMC import *

@vdm_module('n1', 'n2')
class fibonacci:
    """
    state State of 
        n1 : nat
        n2 : nat
        init s == s = mk_State(0, 1)
    end
    operations
        next : () ==> nat
        next() == (dcl n : nat := n1 + n2; n1 := n2; n2 := n; return n)
        post RESULT = n1~ + n2~ and n1 = n2~ and n2 = RESULT;
        prev : () ==> nat
        prev() == (dcl n : nat := n2 - n1; n2 := n1; n1 := n; return n2)
        post n1 + n2 = n2~ and n2 = n1~ and n2 = RESULT;
    """
    def __init__(self):
        self.n1 = 0
        self.n2 = 1
    @vdm_method
    def next(self):
        pass
    @vdm_test
    def prev(self):
        n = self.n2 - self.n1
        self.n2 = self.n1
        self.n1 = n
        return self.n2

Here, a VDM-SL spec of fibonacci numbers is embedded as a docstring of the python fibonacci class. The arguments of the @vdm_module decorator are state variables to be associated with instance variables of the python object.

The next method has no python implementation. The @vdm_method decorator specifies that this method is animated by the VDM-SL spec. In this particular case, next() in VDM-SL is evaluated and the resulting nat number is converted into python's int value.

The prev method has a python implemenation. The @vdm_test decorator specifies that invoking this method will automatically evaluate the VDM-SL spec along with the python method, and all state variables and resulting value is compared with python's counterparts.

>>> from fibonacci import fibonacci
>>> f = fibonacci()
>>> f.next()
1
>>> f.next()
2
>>> f.next()
3
>>> f.next()
5
>>> f.prev()
3
>>> f.prev()
2

Enjoy!


This project is partly supported by Grant-in-Aid Scientific Research (C) 26330099

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.