Re: [tlaplus] C0 and TLAPLUS

[Martin <martin...@xxxxxxxxxxxxxx>]

Hello,

I had a quick look at C0 and it looks definitely easier to verify than
pure C (e.g. there is no typecasting). If I understand correctly, the
difference to Pluscal is that C0 has explicit memory management, an I/O
library and contracts.

I'm not sure what role you envision for C0 in combination to TLA though
- it might be easier to teach verification when you already know about
assertions and loop invariants. But the other features of C0 complicate
the verification process - in particular you need to prove that memory
management is correct and are bound to C-like data-structures like
null-terminated strings. I believe they distract a student from
reasoning on the actual algorithm and put the focus on the book-keeping
a C like language enforces.

Insofar I'd prefer to teach a purely functional language like Haskell,
which is closer to logic (e.g. that it doesn't have assignment or the
way list comprehensions resemble mathematical set comprehensions) and
better suited to reasoning on parallelism. At least I have the feeling
that the gap between C0 and Pluscal is esier to understand than that
between Pluscal and TLA.

What I would find interesting though would be code-generation from a
reasonable subset of Pluscal (full Pluscal allows arbitrary TLA
expressions like  CHOOSE x : ~(x \in Nat) - which shouldn't be
translated to an iteration on the whole set of natural numbers).

cheers, Martin

On 09/05/2016 07:30 PM, 'fl' via tlaplus wrote:
> 
> I think that Franck Pfenning C0
> 
>> http://c0.typesafety.net/
> 
>> http://www.cs.cmu.edu/~fp/papers/pic11.pdf
> 
>> http://www.cs.cmu.edu/~fp/
> 
> and concurrent C0 (but it doesn't see that it can be already downloaded)
> 
>> http://www.cs.cmu.edu/~fp/papers/cc016.pdf
> 
> is worth being used with TLAPLUS.
> 
> 
> C0 is a simplified version of C. You don't have the burden of the
> ununderstandable standard of C and
> you benefit however of a language that looks like C, has pointers and so
> on. It is so close to C that the
> bridge between the two languages is easily crossed. And you also have a
> contract language. Then it
> can be used rigorously.
> 
> It is clear that it is THE language that can be used to teach imperative
> languages.
> 
> It can be used with PLUSCAL. I think the two interface well. You teach
> C0 first then you teach
> PLUSCAL. And you show how to combine both. How to design your program
> with PLUSCAL,
> animate it with TLC, prove it with TLAPS and then translate it into C0.
> You can also show
> how to translate the TLAPLUS ASSUME into C0 contract.
> 
> That way you have a complete combined envrionment, PLUSCAL for the
> design and C0 for
> the implementation. With the rigor guaranteed at every level.
> 
> -- 
> FL
> 
> -- 
> You received this message because you are subscribed to the Google
> Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to tlaplus+u...@xxxxxxxxxxxxxxxx
> <mailto:tlaplus+u...@xxxxxxxxxxxxxxxx>.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx
> <mailto:tla...@xxxxxxxxxxxxxxxx>.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.