[plt-scheme] Re: Expressivity gap between formal methods and PL's

From: Shriram Krishnamurthi (sk at cs.brown.edu)
Date: Sat May 2 08:47:22 EDT 2009

Dear wooks,

Having gone back and re-read the thread, I can see why Paulo has
difficulty telling what you had in mind, because it keeps slipping and
sliding.  You've switched from talking about testing to implementing
back to testing again.  With such slipperiness of expression, you
either badly need a spec language or you will have great difficulty
with one, or both. (-:

If what you want to do is generate tests from formal specifications,
that's a simpler problem with much better-developed solutions.  For a
concrete example, look at Marinov and Khurshid's "TestEra" (which too
is based on Alloy), and follow pointers backward and forward.


Posted on the users mailing list.