ViennaTalk and assertch: Building lightweight formal methods environments on pharo 4

Tomohiro Oda, Keijiro Araki, Peter Gorm Larsen

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

It is possible to make Integrated Development Environments supporting formal methods that can be as flexible as the support for dynamic programming languages. This paper contributes with a demonstration employing different support environments for the Vienna Development Method Specification Language (VDMSL) and design by contract for visual programming language. This includes ViennaTalk developed on top of Pharo 4 providing Smalltalk-styled LIVE browsers, VDM-SL interpreters, Smalltalk code generators, UI prototyping environments and a prototypeWeb API server to enable rigorous and flexible modeling during exploratory phases of software development. ViennaTalk uses the Slot mechanism in Pharo to test invariant assertions on instance variables in Smalltalk objects generated from VDM-SL specifications. In addition, we present a plugin named Assertch for Phratch, a scratch-clone visual programming environment on top of Pharo 4, that provides assertion blocks for designing and debugging a series of blocks. Both ViennaTalk and Assertch combine flexible live modeling or coding while still supporting rigorous checking. ViennaTalk has been evaluated by experienced professional engineers of VDM-SL while Assertch has been evaluated by undergraduate students of computer science. ViennaTalk and Assertch both demonstrate that Pharo and its contemporary features support rigorous modeling in formal specification languages as well as flexible prototyping in Smalltalk.

Original languageEnglish
Title of host publicationIWST 2016 - Proceedings of the 11th International Workshop on Smalltalk Technologies, in conjunction with the 24th International Smalltalk Joint Conference
PublisherAssociation for Computing Machinery, Inc
ISBN (Electronic)9781450345248
DOIs
Publication statusPublished - Aug 23 2016
Event11th International Workshop on Smalltalk Technologies, IWST 2016 - Prague, Czech Republic
Duration: Aug 23 2016Aug 24 2016

Publication series

NameIWST 2016 - Proceedings of the 11th International Workshop on Smalltalk Technologies, in conjunction with the 24th International Smalltalk Joint Conference

Other

Other11th International Workshop on Smalltalk Technologies, IWST 2016
CountryCzech Republic
CityPrague
Period8/23/168/24/16

All Science Journal Classification (ASJC) codes

  • Signal Processing
  • Computer Networks and Communications
  • Computer Science Applications

Fingerprint Dive into the research topics of 'ViennaTalk and assertch: Building lightweight formal methods environments on pharo 4'. Together they form a unique fingerprint.

Cite this