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

[Oliver Bandel <oliver@first.in-berlin.de>]

Hello Nuno,


many, many thanks, these three are very good hints!


Best Regards,
    Oliver



Zitat von Nuno Gaspar <nmpgaspar@gmail.com> (Tue, 22 Jul 2014 10:25:55 +0200)

> 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.
>
> --
> 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