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

On Thu, Apr 30, 2009 at 6:23 PM, wooks <wookiz at hotmail.com> wrote:
>
> Is the availability of an executable formal specification the
> exception or the rule?
>

I cannot say for certain but I would guess it is the exception.

> Regardless an executable specification may not be suitable for
> deployment for reasons
> stated in the original post, so some translation may be inevitable.
>
> The primary scenario I have in mind is what to do when there is no
> executable specification.
>

What do you mean, what to do? If we are here thinking about formal
specification of software, then there really is nothing you can do.
You specify your model just to get a better understand of how it works
in a formal language and then you implement it in a programming
language trying to maintain invariants. Contracts might help but I
don't know about any research in this direction.

>
>
> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>



-- 
Paulo Jorge Matos - pocmatos at gmail.com
Webpage: http://www.personal.soton.ac.uk/pocm