{'fraction_non_alphanumeric': 0.019444444444444445, 'fraction_numerical': 0.0, 'mean_word_length': 5.974193548387097, '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}}
Extended Static Checking by Strategic Rewriting of Pointfree Relational Expressions

Binary relational algebra provides semantic foundations for major areas of computing, such as database design, state-based specification, and functional programming. Remarkably, static checking support in these areas fails to exploit the full semantic content of relations. In particular, properties such as the simplicity or injectivity of relations are not statically enforced in operations that manipulate relations, such as database queries, state transitions, or composition of functional components. We describe how a pointfree treatment of relations, their properties, their operators, and the laws that govern them can be captured in a type-directed strategic rewriting system for transformation of relational expressions. This rewriting tool can be used to simplify relational proof obligations and ultimately reduce them to tautologies. We demonstrate how such reductions provide extended static checking (ESC) for design contraints commonly found in software modeling and development.