Re: [isabelle] Program verification using denotational semantics



I have done.work, over the years, on both program verification and denotational semantics. If you are using the axiomatic method, the point is to use the denotational description of a language in order to prove that the axioms hold in that language under certain conditions. We should all be aware that the axioms don't always hold; even the Assignment Axiom doesn't always hold in the presence of side effects. 

Sent from my iPhone

> On Jan 13, 2016, at 10:27 AM, cl-isabelle-users-request at lists.cam.ac.uk wrote:
> 
> Send Cl-isabelle-users mailing list submissions to
>    cl-isabelle-users at lists.cam.ac.uk
> 
> To subscribe or unsubscribe via the World Wide Web, visit
>    https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users
> or, via email, send a message with subject or body 'help' to
>    cl-isabelle-users-request at lists.cam.ac.uk
> 
> You can reach the person managing the list at
>    cl-isabelle-users-owner at lists.cam.ac.uk
> 
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of Cl-isabelle-users digest..."
> 
> 
> Today's Topics:
> 
>   1. Re:  building session confuses paths to theories (Walther Neuper)
>   2. Re:  Isabelle2016-RC0: HiDPI + Linux (Makarius)
>   3. Re:  Isabelle2016-RC0: HiDPI + Linux (Makarius)
>   4. Re:  Isabelle2016-RC0: HiDPI + Linux (Makarius)
>   5.  program verification using denotational semantics (Buday Gergely)
>   6. Re:  Isabelle2016-RC0: HiDPI + Linux (Corey Richardson)
>   7. Re:  Isabelle2016-RC0: HiDPI + Linux (Corey Richardson)
> 
> 
> ----------------------------------------------------------------------
> 
> Message: 1
> Date: Wed, 13 Jan 2016 15:04:39 +0100
> From: Walther Neuper <wneuper at ist.tugraz.at>
> Subject: Re: [isabelle] building session confuses paths to theories
> To: cl-isabelle-users at lists.cam.ac.uk
> Message-ID: <56965977.1020508 at ist.tugraz.at>
> Content-Type: text/plain; charset=utf-8; format=flowed
> 
> 
> 
>> On 2016-01-12 13:23, Peter Lammich wrote:
>> This error often happens if you re-arrange theories in the build.
>> 
>> Isabelle only seems to check the theory path the first time it sees the
>> import, any further imports of the same theory seem to be somewhat path
>> insensitive ... so wrong import paths may slip through, and only
>> manifest them later.
> Thank you, Peter, for the helpful explanation.
> 
> It is hard here to find out, what is really going on, by we have already 
> partial success:
>     https://intra.ist.tugraz.at/hg/isa/rev/ebf4a8a63371
> 
> Walther
> 
> 
> 
> ------------------------------
> 
> Message: 2
> Date: Wed, 13 Jan 2016 14:54:56 +0100 (CET)
> From: Makarius <makarius at sketis.net>
> Subject: Re: [isabelle] Isabelle2016-RC0: HiDPI + Linux
> To: Corey Richardson <corey at octayn.net>
> Cc: isabelle-users at cl.cam.ac.uk
> Message-ID:
>    <alpine.LNX.2.00.1601131453540.48369 at lxbroy10.informatik.tu-muenchen.de>
>    
> Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
> 
> For information, here is a related thread on the jedit-devel mailing list 
> on "Global font scaling?" 
> http://sourceforge.net/p/jedit/mailman/message/34376635/
> 
> 
>    Makarius
> 
> 
> 
> ------------------------------
> 
> Message: 3
> Date: Wed, 13 Jan 2016 14:53:00 +0100 (CET)
> From: Makarius <makarius at sketis.net>
> Subject: Re: [isabelle] Isabelle2016-RC0: HiDPI + Linux
> To: Corey Richardson <corey at octayn.net>
> Cc: isabelle-users at cl.cam.ac.uk
> Message-ID:
>    <alpine.LNX.2.00.1601131437390.48369 at lxbroy10.informatik.tu-muenchen.de>
>    
> Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
> 
>> On Tue, 12 Jan 2016, Corey Richardson wrote:
>> 
>> Isabelle/jEdit with this release still doesn't work very well with "HiDPI"
>> screens on Linux. For example, I've attached a screenshot of Isabelle/jEdit in
>> front of a terminal. My screen is 3200x1800. It's quite difficult to use,
>> although turning up the font size in the editor as I've done helps somewhat.
>> The larger text in the image I consider comfortable but small, whereas the
>> smaller text is near unreadable.
>> 
>> I realize this is more of a platform/jdk concern -- I found
>> https://bugs.openjdk.java.net/browse/JDK-8055212 and
>> https://bugs.openjdk.java.net/browse/JDK-8137571, which are slated for
>> inclusion in the JDK9. However, if a workaround were possible in
>> Isabelle/jEdit, I would appreciate it.
> 
> That is an interesting article about ongoing work on Java 9.  I estimate 
> that Oracle will require 1-2 more years to make Java 9 practically 
> available for everyone.  For Isabelle2016 we are shipping Java 8 for the 
> first time, and I am still hoping for further consolidation next week.
> 
> 
> As I am using a 3840x2160 display myself since Dec-2014, I've spent a lot 
> of time during last year to make jEdit 5.3.0 work properly with that. 
> This is used for Isabelle2016-RC0, and its NEWS file advertizes improved 
> 4K display support explicitly.
> 
> These changes are mainly relevant for Windows 7, 8.1, 10, due to the way 
> the system DPI configuration is applied to its native GUI in AWT/Swing.
> 
> For Linux, the approach to GUI scaling works the same for Isabelle2015 and 
> Isabelle2016, as described in the Isabelle/jEdit manual section "2.1.2 
> Displays with very high resolution".  The manual is not yet updated in 
> Isabelle2016-RC0, so the text and the screenshot is still that of 
> Isabelle2015.  Your screenshot shows Linux with Metal look&feel, so this 
> should definitely work as described.
> 
> 
> Just yesterday, I've updated the screenshots for the coming release.  See 
> https://bitbucket.org/isabelle_project/isabelle-release/commits/b855771b39798fa3a5b0b88a82eeabc87e184e36#chg-src/Doc/JEdit/document/isabelle-jedit-hdpi.png 
> as a proof that the rendering quality did not change with the (scalable) 
> Metal look&feel.
> 
> Personally, I am often using GTK look&feel, with GTK's own font and GUI 
> scaling.  But that depends on so many other side-conditions, that I don't 
> dare to make it the default.
> 
> 
>    Makarius
> 
> 
> 
> 
> ------------------------------
> 
> Message: 4
> Date: Wed, 13 Jan 2016 15:35:46 +0100 (CET)
> From: Makarius <makarius at sketis.net>
> Subject: Re: [isabelle] Isabelle2016-RC0: HiDPI + Linux
> To: Corey Richardson <corey at octayn.net>
> Cc: isabelle-users at cl.cam.ac.uk
> Message-ID:
>    <alpine.LNX.2.00.1601131531210.63642 at lxbroy10.informatik.tu-muenchen.de>
>    
> Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
> 
>> On Tue, 12 Jan 2016, Corey Richardson wrote:
>> 
>> For example, I've attached a screenshot of Isabelle/jEdit in front of a 
>> terminal.
> 
> What is also interesting with the screenshot: you are using the canonical 
> GUI layout for what would have been called "3-buffer model" in Proof 
> General 3 or 4.  I.e. there is the main text area with separate dockable 
> windows for Output and State.
> 
> How did you figure that out?  The ANNOUNCE and NEWS files mention that, 
> but the Isabelle/jEdit documentation still needs updating.  There is also 
> the standard question how much documentation people actually read.
> 
> My hope and my guess is that looking closely at the default startup GUI of 
> Isabelle/jEdit should make it clear to experienced users how to arrange 
> these windows in a way they see fit.
> 
> 
>    Makarius
> 
> 
> 
> 
> ------------------------------
> 
> Message: 5
> Date: Wed, 13 Jan 2016 15:41:27 +0100
> From: Buday Gergely <gbuday at karolyrobert.hu>
> Subject: [isabelle] program verification using denotational semantics
> To: "cl-isabelle-users at lists.cam.ac.uk"
>    <cl-isabelle-users at lists.cam.ac.uk>
> Message-ID:
>    <C32D3449D568C445AB18C60817FABFE10144E5188615 at ingrid.foiskola.krf>
> Content-Type: text/plain; charset="us-ascii"
> 
> Hi,
> 
> is there extensive literature on using denotational semantics for program verification?
> 
> With a quick search I have found
> 
> Wolfgang Polak. Program verification based on denotational semantics. In Conference Record of the Eighth ACM Symposium on Principles of Programming Languages, pages 149-158. ACM, January 1981.
> 
> http://www.pocs.com/Papers/POPL-81.pdf
> 
> and
> 
> The Foundations of Program Verification, 2nd Edition Jacques Loeckx, Kurt Sieber
> ISBN: 978-0-471-91282-8
> 
> and this course:
> 
> https://moves.rwth-aachen.de/teaching/ss-15/sv-sw/
> 
> Also, is there a practical program verification tool for some language using denotational semantics?
> 
> - Gergely
> 
> 
> 
> ------------------------------
> 
> Message: 6
> Date: Wed, 13 Jan 2016 10:22:06 -0500
> From: Corey Richardson <corey at octayn.net>
> Subject: Re: [isabelle] Isabelle2016-RC0: HiDPI + Linux
> To: Makarius <makarius at sketis.net>
> Cc: isabelle-users at cl.cam.ac.uk
> Message-ID: <20160113152206.GA8856 at roger>
> Content-Type: text/plain; charset="utf-8"
> 
>> On Wed, Jan 13, 2016 at 03:35:46PM +0100, Makarius wrote:
>> How did you figure that out?  The ANNOUNCE and NEWS files mention that, but
>> the Isabelle/jEdit documentation still needs updating.  There is also the
>> standard question how much documentation people actually read.
> 
> I am embarrassed to admit I have not read that much documentation yet for this
> release, and only slightly more for Isabelle2015.
> 
>> My hope and my guess is that looking closely at the default startup GUI of
>> Isabelle/jEdit should make it clear to experienced users how to arrange
>> these windows in a way they see fit.
> 
> I did find it easy to click around until I got what I thought was closer to
> the layout I use with Isabelle2015 on my desktop (with a more traditional
> display), though I had not yet achieved it.
> 
> In general my experience with Isabelle/jEdit has been very positive. The only
> issue I have had with it previously is trying to use a custom font but still
> have symbols from IsabelleText. I found a previous thread about this feature:
> 
> https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-September/msg00009.html
> 
> and decided to just use IsabelleText, as it is acceptable.
> 
> --
> cmr
> +16032392210
> http://octayn.net/
> -------------- next part --------------
> A non-text attachment was scrubbed...
> Name: not available
> Type: application/pgp-signature
> Size: 473 bytes
> Desc: not available
> Url : https://lists.cam.ac.uk/pipermail/cl-isabelle-users/attachments/20160113/ceb12ff5/attachment.sig 
> 
> ------------------------------
> 
> Message: 7
> Date: Wed, 13 Jan 2016 10:27:00 -0500
> From: Corey Richardson <corey at octayn.net>
> Subject: Re: [isabelle] Isabelle2016-RC0: HiDPI + Linux
> To: Makarius <makarius at sketis.net>
> Cc: isabelle-users at cl.cam.ac.uk
> Message-ID: <20160113152700.GB8856 at roger>
> Content-Type: text/plain; charset="utf-8"
> 
>> On Wed, Jan 13, 2016 at 02:53:00PM +0100, Makarius wrote:
>> For Linux, the approach to GUI scaling works the same for Isabelle2015 and
>> Isabelle2016, as described in the Isabelle/jEdit manual section "2.1.2
>> Displays with very high resolution".  The manual is not yet updated in
>> Isabelle2016-RC0, so the text and the screenshot is still that of
>> Isabelle2015.  Your screenshot shows Linux with Metal look&feel, so this
>> should definitely work as described.
> 
> Thank you for the pointers. Tweaking the font sizes in use helps tremendously,
> although some "widgets" such as checkboxes and scrollbars are somewhat small,
> as are most icons.
> 
>> Personally, I am often using GTK look&feel, with GTK's own font and GUI
>> scaling.  But that depends on so many other side-conditions, that I don't
>> dare to make it the default.
> 
> I will experiment with that to see if I can make it work, as I imagine that
> has a better result.
> 
> --
> cmr
> +16032392210
> http://octayn.net/
> -------------- next part --------------
> A non-text attachment was scrubbed...
> Name: not available
> Type: application/pgp-signature
> Size: 473 bytes
> Desc: not available
> Url : https://lists.cam.ac.uk/pipermail/cl-isabelle-users/attachments/20160113/cb7aee62/attachment.sig 
> 
> End of Cl-isabelle-users Digest, Vol 127, Issue 16
> **************************************************




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.