From 2d5f0020a5e76d3f9db475cbf9e7b53dd3cadfe2 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 27 Jul 2022 14:08:14 +0200
Subject: [PATCH] [stdlib] Rework some style.
---
stdlib/caisar.mlw | 12 +++++++++---
tests/simple_ovo.t | 9 ++++-----
2 files changed, 13 insertions(+), 8 deletions(-)
diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw
index 7840d048..4010d785 100644
--- a/stdlib/caisar.mlw
+++ b/stdlib/caisar.mlw
@@ -28,13 +28,19 @@ end
theory SVM
use ieee_float.Float64
use int.Int
+
type input_type = int -> t
type output_type = int
- type svm = {app : input_type -> output_type; num_input: int; num_classes: int}
- predicate dist_linf (a: input_type) (b: input_type) (eps:t) (n: int) =
+ type svm = {
+ app : input_type -> output_type;
+ num_input: int;
+ num_classes: int;
+ }
+
+ predicate linfty_distance (a: input_type) (b: input_type) (eps:t) (n: int) =
forall i. 0 <= i < n -> .- eps .< a i .- b i .< eps
predicate robust_to (svm: svm) (a: input_type) (eps: t) =
- forall b. dist_linf a b eps svm.num_input -> svm.app a = svm.app b
+ forall b. linfty_distance a b eps svm.num_input -> svm.app a = svm.app b
end
diff --git a/tests/simple_ovo.t b/tests/simple_ovo.t
index 3db8856e..03649045 100644
--- a/tests/simple_ovo.t
+++ b/tests/simple_ovo.t
@@ -27,12 +27,11 @@ Test verify
$ caisar verify -L . --format whyml --prover=SAVer --dataset-csv=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
- > use TestSVM.SVMasArray
- > use ieee_float.Float64
- > use caisar.SVM
+ > use TestSVM.SVMasArray
+ > use ieee_float.Float64
+ > use caisar.SVM
>
- > goal G: forall a : input_type.
- > robust_to svm_apply a (8.0:t)
+ > goal G: forall a : input_type. robust_to svm_apply a (8.0:t)
> end
> EOF
<autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
--
GitLab