Skip to content

runtimeverification/python-semantics

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

See INSTALL.md for installation instructions and LICENSE for licensing information.

Quick overview

  • kpython is meant to to act a lot like python3.3. You use it and run programs the same way, although not all functionality of python3.3 is supported. For example, there is no interactive interpreter and many language features are not yet complete.
  • For most programs, to run them you only need to run kpython program.py <args> and everything will work.
  • Because kpython does not yet support the print function, you will likely not see any visible side effect of running your program once it is complete, other than the default output of krun itself. However, the program will still have executed, and you can examine the resulting configuration, including the heap, by examining the output of krun on stdout, which is very large.
  • If you are an advanced user, you may wish to modify some of the parameters that Python uses internally. For example, if you want to run a program under 32-bit python, you can uncomment line 16 of kpython to do this. If you want to decrease the frequency with which garbage collection is performed, you can increase the value of $GC\_THRESHOLD on line 17.
  • If you try to run a program for which semantics have not been given yet, the program will either get stuck or terminate with an exception. A program that terminates with an exception should have raise at the top of the k cell in the output, and a program that terminates cleanly should have an empty k cell. Any other k cell indicates a program that did not behave correctly. If you encounter this, please submit an issue to the issue tracker on Github, if one is not already present. Attach the program you executed, the call to kpython, and the file .k/krun/maude_out in the repository directory. It may simply be that semantics for a feature are not complete yet, but we would still like you to let us know.

Testing the semantics

The programs directory includes many of the tests we've used to build confidence in the correctness of our semantics. To run our main test suite, use the command make test.

We also include the test suites from two other Python semantics, each of which having been updated to work with Python 3.3. To run these test suites, you may use the commands cd programs/politz; make and cd programs/smeding; make.

Important files

  • bootstrapped.bin: This file is generated by the Makefile and contains the configuration of the semantics immediately prior to creation of the code object of the program being executed (i.e., after all the builtin objects have been added to the heap)
  • kpython: The main executable. As previously noted, it is intended to behave like python3.3, however, it is not by any means complete in its functionality yet.
  • parse.py: The script used to parse Python programs and generate K ASTs.
  • python.k: The main K file of the semantics.

About

The semantics of Python in K

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published