The general idea of VyPR is that the developer writes queries over specific functions in a Python program. These queries take the form of properties that should hold at runtime. VyPR decides at runtime whether these properties are satisfied. The results of the queries are given in the form of data describing the satisfaction by the program of the properties.
Queries are written in a central file called VyPR_queries.py in the root of a project's directory structure. This file is written in Python using VyPR's query building library as such:
verification_conf = {
"package.module" : {
"class.method" : [
Forall(
q = changes('x')
).Check(
lambda q : (
q.next_call('g').duration() <= 0.1
)
)
]# class.method
}# package.module
}# verification_conf
In order to tell VyPR where to apply instrumentation and subsequently query at runtime, you need to give the path to each function that you want to monitor.
In the query above, the first level strings tell VyPR which module to look inside and the second level strings tell VyPR which function inside that module.
In order to write a query, you should: