CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Interfacing dynamically typed languages and the why tool: Reasoning about lists and tuples

Claudio Amaral (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; M. Florido ; Patrik Jansson (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Proceedings of the 2011 ACM SIGPLAN Erlang Workshop, Tokyo, 23 September 2011 p. 92-93. (2011)
[Konferensbidrag, refereegranskat]

Formal software verification is currently contributing to new generations of software systems that are proved to follow a given specification. Unfortunately, most dynamically typed languages lack the tools for such reasoning. We present a tool used to help verify some user specified properties on a small language. The process is based on functional contracts with annotations on the source code that later are transformed into logic goals that need to be proved in order to conclude that the program meets its specification. As part of the tool we also present a term model for dynamically typed data structures.

Nyckelord: erlang, verification conditions, why tool



Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2011-12-20. Senast ändrad 2014-09-02.
CPL Pubid: 150538

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)