A Formal Semantics of Python 3.3

This thesis by Dwight Guth, completed in 2013 at the University of Illinois at Urbana-Champaign under the supervision of Grigore Rosu, demonstrates the feasibility of formalizing the operational semantics of complex, real-world programming languages using the K Semantic Framework. Python was chosen as the target language due to its widespread popularity, its complex dynamic semantics, and the challenge it poses to formal methods. The work presents a partial but executable semantics of Python 3.3, the latest version at the time, and represents one of the earliest efforts to apply K to a dynamically-typed, high-level scripting language. The resulting semantics can serve as both an interpreter and a foundation for program analysis, making it a practical tool rather than merely a theoretical artifact.

The K Semantic Framework ($\mathbb{K}$) is a rewrite-based framework for defining programming language semantics. In K, a language semantics is specified as a set of rewrite rules that operate over a configuration -- a structured representation of the program state organized into nested cells. For Python, this configuration must capture the evaluation context, the environment mapping variable names to memory locations, the store mapping locations to values, the object heap modeling Python's uniform object model, and various auxiliary structures for handling control flow. The key advantage of K is that once a semantics is defined, it automatically yields an interpreter, a state-space explorer, and a foundation for deductive verification. The notation $\langle \cdot \rangle_{\text{cell}}$ denotes configuration cells, and rewrite rules take the form $l \Rightarrow r$ within specific cell contexts.

Python's dynamic nature presents unique challenges for formal semantics. Every value in Python is an object, and the language's object model involves a sophisticated attribute resolution mechanism based on the Method Resolution Order (MRO), which uses the C3 linearization algorithm for multiple inheritance. The semantics must accurately model how attribute lookup traverses the class hierarchy, how descriptors (objects implementing __get__, __set__, or __delete__) intercept attribute access, and how metaclasses control class creation. Guth's semantics formalizes these mechanisms faithfully, capturing the subtleties that distinguish Python from simpler languages. The dynamic typing system, where types are themselves first-class objects, adds another layer of complexity that the formalization must address.

The semantics covers a substantial portion of Python 3.3's feature set, including core data types (integers, floats, strings, booleans, lists, tuples, dictionaries, sets), control flow constructs (if/elif/else, while, for loops with break/continue), function definitions with default arguments and keyword arguments, class definitions with single and multiple inheritance, exception handling with try/except/finally and the raise statement, and generator expressions with the yield keyword. For each feature, the formalization follows Python's reference implementation (CPython) to ensure behavioral fidelity. The semantics handles Python's distinctive features such as list comprehensions, generator expressions that lazily produce values, and the with statement for context management, each of which requires careful modeling of the underlying iterator protocol.

The K semantics of Python 3.3 provides not just an interpreter, but a foundation for formal reasoning about Python programs, including the ability to explore sources of nondeterminism in the language specification.

Testing and validation form a critical part of the thesis. The semantics was thoroughly tested against a suite of unit tests designed to exercise individual language features and their interactions. On the features that have been completed, the K-based interpreter performs as well as the reference implementation CPython, producing identical results for all test cases. This empirical validation provides confidence that the formalization accurately captures the intended semantics of Python 3.3 as defined by the language specification and as implemented by CPython. The test-driven approach ensures that each semantic rule corresponds to observable behavior rather than abstract specifications that might diverge from practice.

While the semantics is acknowledged to be incomplete -- certain advanced features such as the full module system, some built-in functions, and portions of the standard library are not covered -- the work demonstrates that the K framework is capable of scaling to real-world languages with complex dynamic semantics. The incompleteness is a practical limitation rather than a fundamental one; the framework is extensible, and additional features can be added incrementally as new semantic rules. The thesis identifies specific areas where the formalization could be extended, providing a roadmap for future work. The modular nature of K definitions means that new rules can be added without modifying existing ones, making the semantics a living artifact that can grow with the language.

The broader significance of this work lies in its contribution to the K framework's portfolio of real-world language semantics. Alongside the formal semantics of C, Java, JavaScript, and the Ethereum Virtual Machine, the Python semantics demonstrates K's versatility as a language-agnostic framework for formal semantics. This has practical implications for program verification, compiler testing, and language design. In the context of Pi2 Labs's technology, such formal semantics serve as the foundation for generating mathematical proofs of program correctness, which can then be translated into cryptographic proofs for verifiable computing. The ability to formally reason about Python programs opens pathways to trustworthy execution of one of the world's most widely-used programming languages.

The work also highlights important methodological lessons for formalizing dynamically-typed languages. Unlike statically-typed languages such as Java, where a clear separation between compile-time and runtime semantics exists, Python's semantics is almost entirely dynamic. Types are determined at runtime, method dispatch depends on the runtime class hierarchy, and even the class creation process can be customized through metaclasses. This means the formal semantics must model a richer runtime state and more complex evaluation rules. The thesis demonstrates that K's configuration-based approach, with its flexible cell structure and context-sensitive rewriting, is well-suited to capturing these dynamic behaviors in a natural and readable way.