[Why3-club] Low level constructs
Per.Lindgren at ltu.se
Mon Aug 15 18:09:52 CEST 2016
On 15 Aug 2016, at 17:07, Neil Evans <n.evans at zepler.net<mailto:n.evans at zepler.net>> wrote:
I'm trying to do a comparison between Why3 and MALPAS, specifically WhyML and the MALPAS Intermediate Language (MALPAS IL). (Knowledge of MALPAS is not important for answering my query but I thought I'd mention it just in case.)
I would like to know to what extent WhyML can represent low-level language constructs such as GOTOs (unconditional jumps to labels) and updates to non-local variables (to model side effects). I've looked at the manual/tutorial but it's not immediately apparent if these sorts of thing are possible or not. These features are available in MALPAS IL but it is now old technology and I'm seeking alternative tools to model instruction sets and assembly code for formal analysis.
To my knowledge you cannot model GOTO in the native WhyML language.
Global variables (per module) can be modelled and used by functions with side effects (“writes” and “reads”).
You may have a look at toccata (http://toccata.lri.fr) there you find a large number of verification examples.
When it comes to modelling other languages/instruction sets in why3, you can have a look at “wp_revisited” (http://toccata.lri.fr/gallery/WP_revisited.en.html) and “double_wp” (http://toccata.lri.fr/gallery/double_wp.en.html), both encode operational semantics and Hoare logic. While wp_revisted has a focus on generating VCs from assertions in the input language, double_wp encodes wps to verify the correctness of a “toy” compiler. Both models a “classic” imp language with assignments conditionals and (while) loops.
An encoding of the ARM instruction set can be found at. http://inforum.org.pt/INForum2012/docs/20120013.pdf. However, quote "As it can be noticed, branching instructions are not included in the grammar rules. This happens due to the fact that sequentialization mechanism removes those instructions from the code of sequential programs.” (I.e, the input program is unrolled (by an external tool) before put to analysis.)
If this is not what you are looking for, you may have a look at Bedrock (http://plv.csail.mit.edu/bedrock/) which is a more extensive “low level programming” framework in Coq. Another encoding of (simple) imperative language (and Hoare logic) in Coq is found in SF (https://www.cis.upenn.edu/~bcpierce/sf/current/index.html), a very good introduction to both Coq and program verification. Also (http://research.microsoft.com/en-us/um/people/nick/coqasm.pdf) shows an encoding of low level instruction (X86) set in Coq. There are probably loads more.
Why3-club mailing list
Why3-club at lists.gforge.inria.fr<mailto:Why3-club at lists.gforge.inria.fr>
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Why3-club