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

On Thu, Apr 30, 2009 at 7:53 PM, wooks <wookiz at hotmail.com> wrote:
>
>
> On Apr 30, 8:25 pm, "Paulo J. Matos" <pocma... at gmail.com> wrote:
>
>>
>> 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.
>>
>
> Well I want to go from having a (hopefully) correct formal spec of my
> system to
> a correctly functioning system.
>

By system I will assume you mean software system...

>>
>> 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.
>>
>
> If I had a formal specification of a system then I'd want to get alot
> more out of it.
>
> So what are the sorts of things I can express in a formal
> specification language that
> do not readily translate to programming languages.
>
> What sorts of things are the biggest threats to the fidelity of the
> translation.
>

For a start, lets say that you need a language that mixes
specification languages + programming languages.
You see, each language varies but formal specification languages are
usually based on a logic + set theory and may _or_ may not have an
execution model.

Alloy is relational logic without an execution model. It's
declarative. You write your model declarative, write a couple of facts
and that's it. FAR, FAAAAAAAAR, away from an 'executable' and
generating an executable directly from an Alloy mode wouldn't even
make sense.

Event-B has [I will simplify it] a state with a set of variables whose
type are one of enumerations, integer set, boolean set, powersets of
types and cartesian product of types. Then it has events which has a
guard and a set of actions which update the variables in the state
atomically. It has an execution model. At each point in time, at least
one event guard needs to be true and an event whose guard is true is
chosen non-deterministically to update the state and loop... [meaning,
choose another event non deterministically].

As you can see these are two distinct languages, both with specific
applications but none afaik was designed to be converted into an
executable program. Event-B would even have a lot of trouble in
modeling software. Some issues are, lack of structures, modules,
non-determinism, to name just a few.

You could convert an eventb model into an executable but it wouldn't
be a proper software package ready to be deployed, far from it.

> Perhaps another way of looking at it is if you decided to implement
> (lets say Z in Scheme/Lisp)
> what constructs would be the most troublesome to implement.
>
>

You got me here.. what do you mean by implementing Z in Scheme/Lisp?
You mean, a specific model of Z or a prover for Z? or a simulator for Z models?

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