About
KPHP is an executable formal semantics for PHP written in
K,
a language definitional framework based on
Rewriting Logic
and
implemented on top of the
Maude system.
KPHP is described in the paper An Executable Formal Semantics of PHP
by
D. Filaretti
and
S. Maffeis, to appear at ECOOP 2014.
An up-to-date, extended version of the paper is available
here.
If you just want to try out KPHP, you can use the Online interface.
All the source files are available in the Download section, together with a Linux-based virtual machine with a fresh working copy of the KPHP distribution and dependencies.
All files are copyright of the authors.
Work funded by EPSRC grant EP1004246/1.
Downloads and Documentation
All KPHP source files are human readable and executable via the K tools
(see the instructions provided in the Documentation section).
Documentation
We provide an informal
documentation
based on examples.
We plan to expand and revise this documentation in the future.
Sources
You can download all the sources
as a single zip file here.
See the Documentation section and the README file included in the
archive for usage information.
Note that it is necessary to obtain a
binary distribution of the K Framework
in order to compile
and execute our semantics. Please get the latest build .
Using the KPHP virtual machine
Alternatively, in case you experience issues installing the K tools
(which is unlikely),
you can use our self-contained Linux-based
virtual machine .
The archive contains the following files:
-
kvm3.vmwarevm : The virtual machine
-
k folder: The K tools
For detailed set-up and usage information, please refer to the
KVM documentation .
Note that the procedure is the same but there is no need to download the KVM or the K tools, as
are already provided by us in this package.
When setting up the shared folders in VMWare (5th bulletpoint in the
"Setting up the KVM" section) you should add the k folder
as well as the folder containing the KPHP sources.