Re: [Caml-list] Program proof - how to do that?

[Nuno Gaspar <nmpgaspar@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2186 bytes --]

You wanna take a look at Hoare Logic:
http://en.wikipedia.org/wiki/Hoare_logic

Then, you can peek Weakest precondiction calculus:
http://en.wikipedia.org/wiki/Predicate_transformer_semantics

And if you're brave, Separation logic.
http://en.wikipedia.org/wiki/Separation_logic

Oh, and if you still some more spare time: Rely/Guarantee. :)

Hope it helps.





2014-07-22 0:37 GMT+02:00 Oliver Bandel <oliver@first.in-berlin.de>:

> Hello,
>
> thanks to all people who answered.
>
> I'm sorry that I can't attend to the logics conference mentioned in on
> answer. Maybe next time.
>
> Would be fine if such events could be mentioned on this list.
>
>
>
> Zitat von David MENTRÉ <dmentre@linux-france.org> (Sat, 19 Jul 2014
> 21:18:04 +0200)
>
>
>  Hello Gabriel,
>>
>> 2014-07-12 14:07, Gabriel Scherer:
>>
>>> I tried to (partially) answer this question in the following
>>> StackOverflow thread:
>>>   http://stackoverflow.com/questions/12937082/ocaml-used-
>>> in-demonstrations
>>>
>>
>>
>> Nice answer.
>>
>> BTW, regarding Why3 in your answer, the current git version of Why3
>> allows to produce OCaml code from a proved WhyML program,
>>
> [...]
>
>
> I here now do hear the first time about "Why3".
>
> Interesting to see what is available in the area of program proof.
>
> But my question also was about the theoretical background of the proof
> stuff.
>
> For example in my exploration of logics I came across model theory and
> tarski semantics.
> Looks interesting to me, something worth exploring in more detail, I think.
>
> Does anybody know more about these topics (theoretically as well as
> if this is used in theorem provers)?
>
>
> Ciao,
>    Oliver
>
>
>
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>



-- 
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600
dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible
life choice.

[-- Attachment #2: Type: text/html, Size: 3691 bytes --]