-
Notifications
You must be signed in to change notification settings - Fork 17
/
_types.py
98 lines (73 loc) · 3.92 KB
/
_types.py
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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
"""Define data structures shared among the modules."""
import inspect
import reprlib
from typing import Callable, Optional, Union, Set, List, Any # pylint: disable=unused-import
import icontract._globals
# pylint: disable=protected-access
class Contract:
"""Represent a contract to be enforced as a precondition, postcondition or as an invariant."""
# pylint: disable=too-many-instance-attributes
def __init__(self,
condition: Callable[..., bool],
description: Optional[str] = None,
a_repr: reprlib.Repr = icontract._globals.aRepr,
error: Optional[Union[Callable[..., Exception], type]] = None,
location: Optional[str] = None) -> None:
"""
Initialize.
:param condition: condition predicate
:param description: textual description of the contract
:param a_repr: representation instance that defines how the values are represented
:param error:
if given as a callable, ``error`` is expected to accept a subset of function arguments
(*e.g.*, also including ``result`` for perconditions, only ``self`` for invariants *etc.*) and return
an exception. The ``error`` is called on contract violation and the resulting exception is raised.
Otherwise, it is expected to denote an Exception class which is instantiated with the violation message
and raised on contract violation.
:param location: indicate where the contract was defined (*e.g.*, path and line number)
"""
# pylint: disable=too-many-arguments
self.condition = condition
signature = inspect.signature(condition)
# All argument names of the condition
self.condition_args = list(signature.parameters.keys()) # type: List[str]
self.condition_arg_set = set(self.condition_args) # type: Set[str]
# Names of the mandatory arguments of the condition
self.mandatory_args = [
name for name, param in signature.parameters.items() if param.default == inspect.Parameter.empty
]
self.description = description
self._a_repr = a_repr
self.error = error
self.error_args = None # type: Optional[List[str]]
self.error_arg_set = None # type: Optional[Set[str]]
if error is not None and (inspect.isfunction(error) or inspect.ismethod(error)):
self.error_args = list(inspect.signature(error).parameters.keys())
self.error_arg_set = set(self.error_args)
self.location = location
class Snapshot:
"""Define a snapshot of an argument *prior* to the function invocation that is later supplied to a postcondition."""
def __init__(self, capture: Callable[..., Any], name: Optional[str] = None, location: Optional[str] = None) -> None:
"""
Initialize.
:param capture:
function to capture the snapshot accepting a single argument (from a set of arguments
of the original function)
:param name: name of the captured variable in OLD that is passed to postconditions
:param location: indicate where the snapshot was defined (*e.g.*, path and line number)
"""
self.capture = capture
args = list(inspect.signature(capture).parameters.keys()) # type: List[str]
if name is None:
if len(args) == 0:
raise ValueError("You must name a snapshot if no argument was given in the capture function.")
elif len(args) > 1:
raise ValueError("You must name a snapshot if multiple arguments were given in the capture function.")
else:
assert len(args) == 1
name = args[0]
assert name is not None, "Expected ``name`` to be set in the preceding execution paths."
self.name = name
self.args = args
self.arg_set = set(args)
self.location = location