1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
/*
** Copyright (C) 2018 Martin Brain
**
** See the file LICENSE for licensing information.
*/
/*
** properties.h
**
** Martin Brain
** martin.brain@cs.ox.ac.uk
** 07/08/14
**
** Macros for specifying invariants in a back-end specific way.
**
** Note that there are two kinds of assertions.
** - Implementation assertions : should be statically or dynamically
** resolvable to bools. Intended to catch cases where the code is
** buggy or being used incorrectly.
** - Algorithm assertions : should be trait::prop and are used
** to document and record properties and assumptions about the
** floating-point computation. Depending on the back-end these may
** be concrete or symbolic and thus handled in different ways.
**
*/
#ifndef SYMFPU_PROPERTIES
#define SYMFPU_PROPERTIES
#define IMPLIES(X,Y) (!(X) || (Y))
#ifndef PRECONDITION
#define PRECONDITION(X) t::precondition(X)
#endif
#ifndef POSTCONDITION
#define POSTCONDITION(X) t::postcondition(X)
#endif
#ifndef INVARIANT
#define INVARIANT(X) t::invariant(X)
#endif
#endif
|
