The Coq mailing list

[Denis Nikiforov <denis.nikif AT gmail.com>]

Hi

I formalized the semantics of the OCL language: https://www.isa-afp.org/entries/Safe_OCL.html

Here is a significantly improved version of the theory: https://github.com/AresEkb/Safe_OCL  

I added new data types, added a concrete syntax, refactored the type system and changed semantics of some operations after discussion with a main OCL contributor.

The project has two goals:

1) Provide a simple reference formalization of a real (non-toy) language for people far from mathematics (for engineers like me). There are a lot of examples of toy languages, but when you start to formalize a more complicated language it's not an easy task. Formalizations of other languages (Java, etc.) are too complicated for me.

2) Improve OCL language itself.

However, I don't have time to finish it. I hope I'll do it in future.

вс, 16 февр. 2020 г. в 06:28, Talia Ringer <tringer AT cs.washington.edu>:

Hi all,

I'm curious if any of you have ever started to verify a system, but then
abandoned that system due to the difficulty of evolving and maintaining
your proofs. If so, I would love for you to share those proof efforts with
me, especially if the code is public.

Thanks!

Talia