From 40c7378e804dddd835ac3d8c1da283716e900e52 Mon Sep 17 00:00:00 2001 From: Calvin Loncaric Date: Mon, 9 Jul 2018 17:32:47 -0700 Subject: [PATCH] Require collections given to arg{min,max} to be non-empty This is additional progress on #23. --- cozy/invariant_preservation.py | 10 ++++++++++ cozy/main.py | 1 + 2 files changed, 11 insertions(+) diff --git a/cozy/invariant_preservation.py b/cozy/invariant_preservation.py index 738e8a6a..892839e2 100644 --- a/cozy/invariant_preservation.py +++ b/cozy/invariant_preservation.py @@ -54,6 +54,16 @@ def check_the_wf(spec : Spec): res.append("at {}: `the` is illegal since its argument may not be singleton".format(pprint(e))) return res +def check_minmax_wf(spec : Spec): + res = [] + for ctx in enumerate_fragments(spec): + e = ctx.e + if isinstance(e, EArgMin) or isinstance(e, EArgMax): + a = ctx.facts + if not valid(EImplies(EAll(a), EUnaryOp(UOp.Exists, e.e).with_type(BOOL))): + res.append("at {}: result is ambiguous since {} could be empty".format(pprint(e), pprint(e.e))) + return res + def check_calls_wf(spec : Spec): res = [] queries = { m.name : m for m in spec.methods if isinstance(m, Query) } diff --git a/cozy/main.py b/cozy/main.py index d82ee449..240be13a 100755 --- a/cozy/main.py +++ b/cozy/main.py @@ -81,6 +81,7 @@ def run(): errors = ( invariant_preservation.check_ops_preserve_invariants(ast) + invariant_preservation.check_the_wf(ast) + + invariant_preservation.check_minmax_wf(ast) + call_errors) if errors: for e in errors: