{'fraction_non_alphanumeric': 0.01765650080256822, 'fraction_numerical': 0.0, 'mean_word_length': 4.909952606635071, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
True small-step reduction for imperative object oriented languages

Traditionally, formal semantic models of Java-like languages use an explicit model of the store which mimics pointers and ram. These low level models hamper understanding of the semantics, and development of proofs about ownerships and other encapsulation properties, since the real (graph) structure of the data is obscured by the encoding. Such models are also inadequate for didactic purposes since they rely on run-time structures that do not exist in the source program --- in order to understand the meaning of an expression in the middle of the execution one is required to visualize the memory structure which is hard to relate to the abstract program state. We present a semantic model for Java-like languages where data is encoded as part of the program rather than as a separate resource. This means that execution can be modelled more simply by just rewriting source code terms, as in semantic models for functional programs. The major challenges that need to be addressed are aliasing, circular object graphs, exceptions and multiple return methods. In this initial proposal we use local variable declarations in order to tackle aliasing and circular object graphs.