Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss

Reasoning with inductive types

31 views
Skip to first unread message

Helmut

unread,
Mar 8, 2012, 3:28:51 PM3/8/12
to
Modern Eiffel is a new language which is syntactically based on Eiffel
but has a lot of concepts of functional languages like Haskell, OCaml
or Coq. Modern Eiffel puts the emphasis on static verification, i.e. a
compiler can statically check that a programm written in Modern Eiffel
meets its specification.

The following article http://softwareverificaton.wordpress.com/2012/03/08/76
describes how Modern Eiffel's proof engine can be used to reason about
inductive types. Reasoning is basic on induction.

ingo.w...@googlemail.com

unread,
Mar 15, 2012, 10:16:50 AM3/15/12
to
Am Donnerstag, 8. März 2012 21:28:51 UTC+1 schrieb Helmut:
> Modern Eiffel is a new language which is syntactically based on Eiffel
> but has a lot of concepts of functional languages like Haskell, OCaml
> or Coq. Modern Eiffel puts the emphasis on static verification, i.e. a
> compiler can statically check that a programm written in Modern Eiffel
> meets its specification.

The specification is written in what language?

Helmut

unread,
Mar 19, 2012, 10:59:26 PM3/19/12
to
The specification is written in Modern Eiffel. Modern Eiffel has
assertions to specify programs.
0 new messages