[Why3-club] Low level constructs

Neil Evans n.evans at zepler.net
Mon Aug 15 17:07:56 CEST 2016


Hello,

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.

Thanks,

Neil.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20160815/6106fc9a/attachment.html>


More information about the Why3-club mailing list