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.
All KPHP source files are human readable and executable via the K tools (see the instructions provided in the Documentation section).
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 .
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
kfolder: 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
as well as the folder containing the KPHP sources.