From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id BC95E7FA56 for ; Wed, 23 Jul 2014 00:31:32 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of oliver@first.in-berlin.de) identity=pra; client-ip=192.109.42.8; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="oliver@first.in-berlin.de"; x-sender="oliver@first.in-berlin.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of oliver@first.in-berlin.de) identity=mailfrom; client-ip=192.109.42.8; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="oliver@first.in-berlin.de"; x-sender="oliver@first.in-berlin.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@einhorn.in-berlin.de) identity=helo; client-ip=192.109.42.8; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="oliver@first.in-berlin.de"; x-sender="postmaster@einhorn.in-berlin.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AmQBAMPlzlPAbSoIf2dsb2JhbABZg2BXBIJ0rnmVNodFAYESFg8BAQsLCggUKYQEAQQBIw8BBTACBBALCxoCCQ8OAgIhJBIZEgeIFQMJCAQJqHaQAQMKhzOBLItygjQWgmKBTgWEcAWUL4ICgU6FRYcFhEOFIWo X-IPAS-Result: AmQBAMPlzlPAbSoIf2dsb2JhbABZg2BXBIJ0rnmVNodFAYESFg8BAQsLCggUKYQEAQQBIw8BBTACBBALCxoCCQ8OAgIhJBIZEgeIFQMJCAQJqHaQAQMKhzOBLItygjQWgmKBTgWEcAWUL4ICgU6FRYcFhEOFIWo X-IronPort-AV: E=Sophos;i="5.01,712,1400018400"; d="scan'208";a="86556746" Received: from einhorn.in-berlin.de ([192.109.42.8]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 23 Jul 2014 00:31:32 +0200 X-Envelope-From: oliver@first.in-berlin.de X-Envelope-To: Received: from yak (yak.in-berlin.de [192.109.42.109]) by einhorn.in-berlin.de (8.14.4/8.14.4/Debian-4) with ESMTP id s6MMVUeD017901 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT) for ; Wed, 23 Jul 2014 00:31:31 +0200 Received: from e178011041.adsl.alicedsl.de (e178011041.adsl.alicedsl.de [85.178.11.41]) by webmail.in-berlin.de (Horde Framework) with HTTP; Wed, 23 Jul 2014 00:31:29 +0200 Date: Wed, 23 Jul 2014 00:31:29 +0200 Message-ID: <20140723003129.Horde.hRwcPoUDlscIPfgrUSHqXg1@webmail.in-berlin.de> From: Oliver Bandel To: caml-list@inria.fr References: <20140712132548.Horde.9ejEAoB3FJ5kFjy5PNSJ9A7@webmail.in-berlin.de> <53CAC46C.2010905@linux-france.org> <20140722003745.Horde.c4SRKyZgSXOQILb6jBJVpA1@webmail.in-berlin.de> In-Reply-To: User-Agent: Internet Messaging Program (IMP) H5 (6.2.0) Content-Type: text/plain; charset=UTF-8; format=flowed; DelSp=Yes MIME-Version: 1.0 Content-Disposition: inline Content-Transfer-Encoding: 8bit Subject: Re: [Caml-list] Program proof - how to do that? Hello Nuno, many, many thanks, these three are very good hints! Best Regards, Oliver Zitat von Nuno Gaspar (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 : > >> 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É (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