Patrick Lühne
|
f169931eac
|
Accept more than one specification file
|
2020-05-29 18:54:47 +02:00 |
Patrick Lühne
|
fc34aadf90
|
Show all predicates used in specification by default
|
2020-05-29 18:41:16 +02:00 |
Patrick Lühne
|
b52ca236e2
|
Handle private predicates in specification
|
2020-05-28 07:27:29 +02:00 |
Patrick Lühne
|
1e55f733d0
|
Minor clean-up
|
2020-05-28 05:03:57 +02:00 |
Patrick Lühne
|
fe277b6773
|
Minor refactoring
|
2020-05-28 05:03:57 +02:00 |
Patrick Lühne
|
491a255811
|
Require supertight programs for backward proof
|
2020-05-28 05:03:56 +02:00 |
Patrick Lühne
|
499fa0c667
|
Add option to specify output color choice
|
2020-05-22 19:33:06 +02:00 |
Patrick Lühne
|
0578e99dc2
|
Finish basic simplifications
|
2020-05-22 18:14:56 +02:00 |
Patrick Lühne
|
3bf981236a
|
Only warn if private predicates are used in specification
|
2020-05-19 12:18:11 +02:00 |
Patrick Lühne
|
80d39c8c0a
|
Check that only input/output predicates are used in specification
|
2020-05-18 02:17:30 +02:00 |
Patrick Lühne
|
82422cc28f
|
Support hiding auxiliary predicates
|
2020-05-13 08:02:04 +02:00 |
Patrick Lühne
|
e0b8b1c854
|
Minor formatting
|
2020-05-11 03:46:20 +02:00 |
Patrick Lühne
|
0d51053b88
|
Move ProofDirection type to separate module
|
2020-05-11 03:46:11 +02:00 |
Patrick Lühne
|
b55bc82b1d
|
Add option for proof direction
|
2020-05-07 02:53:48 +02:00 |
Patrick Lühne
|
15769d58b3
|
Add missing file
|
2020-05-06 21:30:27 +02:00 |
Patrick Lühne
|
b14f620235
|
Implement proof mechanism
|
2020-05-06 00:13:43 +02:00 |
Patrick Lühne
|
e118442e16
|
Work in progress
|
2020-05-05 19:40:57 +02:00 |