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

Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System

B. Fetscher ; Koen Claessen (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Michal H. Palka (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; John Hughes (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; R. B. Findler
Lecture Notes in Computer Science: 24th European Symposiumon Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015; London; United Kingdom; 11 April 2015 through 18 April 2015 (0302-9743). Vol. 9032 (2015), p. 383-405.
[Konferensbidrag, refereegranskat]

This paper presents a generic method for randomly generating well-typed expressions. It starts from a specification of a typing judgment in PLT Redex and uses a specialized solver that employs randomness to find many different valid derivations of the judgment form. Our motivation for building these random terms is to more effectively falsify conjectures as part of the tool-support for semantics models specified in Redex. Accordingly, we evaluate the generator against the other available methods for Redex, as well as the best available custom well-typed term generator. Our results show that our new generator is much more effective than generation techniques that do not explicitly take types into account and is competitive with generation techniques that do, even though they are specialized to particular type-systems and ours is not.



Denna post skapades 2015-10-21. Senast ändrad 2016-06-29.
CPL Pubid: 224572

 

Läs direkt!


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