{'fraction_non_alphanumeric': 0.021759697256385997, 'fraction_numerical': 0.0, 'mean_word_length': 5.6125, '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}}
An alternative approach to handling nondeterminism in model-oriented data-refinement

This paper investigates data-refinement by forward and backward simulations for model-oriented specifications whose semantics is given by partial relations. The most well-known example of such a semantics is that for Z. The standard model-theoretic characterisation of refinement is a relational approach based on totalisation and lifting. We contrast this, and relate it to, a new approach inspired by various concepts in algebraic paradigms and type theory (adapted into a framework based on classical logic) for handling nondeterminism and under specification in data-refinement. We provide a new characterisation of refinement based on extracting a set of (deterministic) "implementations", each of which models the specification in question. We examine a means by which data simulations interact with this notion and demonstrate that each of the ensuing simulation-based theories is equivalent to the corresponding standard relational characterisation of refinement.