A formal semantics of Python 3.3

This thesis demonstrates the ability to formalize the operational semantics of complex programming languages in the K Semantic Framework, which provides an interpreter as well as analysis tools for exploring the state space of programs and performing static reasoning about programs. This is demonstrated by means of a partial semantics for the latest version of the popular Python programming language. With additional effort, this semantics will allow users to reason about Python programs, including sources of nondeterminism in the Python language specification, and formal reasoning about their behavior. While the semantics is incomplete, it is executable and has been thoroughly tested against a number of unit tests, and will be demonstrated to perform as well as the reference implementation of Python, CPython, on those features which have been completed. On these features, it also performs as well as or better than other comparable operational semantics of Python.

Name thesis:degree_name

M.S.

Level thesis:degree_level

Thesis

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2013

Author dc:creator

• Guth, Dwight

Contributors dc:contributor

• Rosu, Grigore

• K framework
• formal semantics
• python
• python3
• python3.3

Statement dc:rights

• Copyright 2013 Dwight Guth

Language dc:language

en

Handle dc:identifier

http://hdl.handle.net/2142/45275

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/45275