/[eiffelstudio]/branches/eth/eve/Src/Delivery/studio/tools/autoproof/base_theory.bpl
ViewVC logotype

Log of /branches/eth/eve/Src/Delivery/studio/tools/autoproof/base_theory.bpl

Parent Directory Parent Directory | Revision Log Revision Log


Links to HEAD: (view) (annotate)
Sticky Revision:

Revision 93378 - (view) (annotate) - [select for diffs]
Modified Thu Nov 14 15:57:08 2013 UTC (5 years, 11 months ago) by julian
File length: 20724 byte(s)
Diff to previous 93349
AutoProof: continued ownership implementation.


Revision 93349 - (view) (annotate) - [select for diffs]
Modified Wed Nov 13 17:15:59 2013 UTC (5 years, 11 months ago) by julian
File length: 20623 byte(s)
Diff to previous 93346
AutoProof: added predicates for partial invariants

Revision 93346 - (view) (annotate) - [select for diffs]
Modified Wed Nov 13 08:05:21 2013 UTC (5 years, 11 months ago) by julian
File length: 20507 byte(s)
Diff to previous 93312
AutoProof: added composite example.

Revision 93312 - (view) (annotate) - [select for diffs]
Modified Tue Nov 12 07:18:14 2013 UTC (5 years, 11 months ago) by julian
File length: 20199 byte(s)
Diff to previous 93306
AutoProof: added "wrap_all" and "unwrap_all" to ownership translation.

Revision 93306 - (view) (annotate) - [select for diffs]
Modified Mon Nov 11 16:45:33 2013 UTC (5 years, 11 months ago) by julian
File length: 19107 byte(s)
Diff to previous 93215
AutoProof: Continued with ownership implementation.
AutoProof: Added PIP example and fixed OOM example.

Revision 93215 - (view) (annotate) - [select for diffs]
Modified Wed Nov 6 15:55:58 2013 UTC (5 years, 11 months ago) by julian
File length: 19048 byte(s)
Diff to previous 93211
AutoProof: continued ownership implementation.

Revision 93211 - (view) (annotate) - [select for diffs]
Modified Tue Nov 5 23:10:23 2013 UTC (5 years, 11 months ago) by julian
File length: 17902 byte(s)
Diff to previous 93206
AutoProof: continued ownership implementation.

Revision 93206 - (view) (annotate) - [select for diffs]
Modified Tue Nov 5 16:52:31 2013 UTC (5 years, 11 months ago) by julian
File length: 17786 byte(s)
Diff to previous 93193
AutoProof: continued ownership implementation.

Revision 93193 - (view) (annotate) - [select for diffs]
Modified Mon Nov 4 16:38:13 2013 UTC (5 years, 11 months ago) by julian
File length: 17537 byte(s)
Diff to previous 93186
AutoProof: continue on ownership implementation.

Revision 93186 - (view) (annotate) - [select for diffs]
Modified Wed Oct 30 16:08:59 2013 UTC (5 years, 11 months ago) by julian
File length: 17527 byte(s)
Diff to previous 92868
AutoProof: continue on ownership implementation.

Revision 92868 - (view) (annotate) - [select for diffs]
Modified Thu Aug 8 14:27:47 2013 UTC (6 years, 2 months ago) by polikarn
File length: 16827 byte(s)
Diff to previous 92742
Meningful tags for ownership checks. Adapted to the new Boogie output format. Handling precondition violations of fake procedures (like update_heap). Ownership checks for heap assignents. Dynamic type of Current is known.

Revision 92742 - (view) (annotate) - [select for diffs]
Modified Wed Jun 26 17:45:24 2013 UTC (6 years, 3 months ago) by polikarn
File length: 16646 byte(s)
Diff to previous 92724
Calling creation version of a procedure from creation expressions; generating creation procedure from default_create; translating MML_SET.is_disjoint.

Revision 92724 - (view) (annotate) - [select for diffs]
Modified Fri Jun 21 11:44:49 2013 UTC (6 years, 4 months ago) by polikarn
File length: 16475 byte(s)
Diff to previous 91348
Renamed depends and dependents into subjects and observers.

Revision 91348 - (view) (annotate) - [select for diffs]
Modified Fri Mar 8 15:59:40 2013 UTC (6 years, 7 months ago) by julian
File length: 16477 byte(s)
Diff to previous 91302
AutoProof: added predicates for arithmetic operations. added suggestion display for two-step verification.



Revision 91302 - (view) (annotate) - [select for diffs]
Modified Wed Feb 27 17:09:56 2013 UTC (6 years, 7 months ago) by julian
File length: 16228 byte(s)
Diff to previous 91213
AutoProof: enabled invariant generation. updated array translation.

Revision 91213 - (view) (annotate) - [select for diffs]
Modified Mon Feb 11 15:42:55 2013 UTC (6 years, 8 months ago) by julian
File length: 16228 byte(s)
Diff to previous 91205
AutoProof: Continued ownership translation.


Revision 91205 - (view) (annotate) - [select for diffs]
Modified Fri Feb 8 16:12:11 2013 UTC (6 years, 8 months ago) by julian
File length: 16066 byte(s)
Diff to previous 91096
AutoProof:
- Continued ownership translation.
- Added boxing/unboxing of integers and booleans.
- Added conversions between integer types.


Revision 91096 - (view) (annotate) - [select for diffs]
Modified Thu Jan 31 16:28:35 2013 UTC (6 years, 8 months ago) by julian
File length: 15570 byte(s)
Diff to previous 90232
Separate Boogie translation for creation routines.
Added incomplete ownership translation.

Revision 90232 - (view) (annotate) - [select for diffs]
Modified Mon Dec 17 16:22:00 2012 UTC (6 years, 10 months ago) by julian
File length: 14154 byte(s)
Diff to previous 90191
Improved command line output of AutoProof

Revision 90191 - (view) (annotate) - [select for diffs]
Modified Fri Dec 14 15:38:20 2012 UTC (6 years, 10 months ago) by julian
File length: 14083 byte(s)
Diff to previous 90127
Updated Boogie theory.

Revision 90127 - (view) (annotate) - [select for diffs]
Modified Fri Dec 7 14:51:15 2012 UTC (6 years, 10 months ago) by julian
File length: 10374 byte(s)
Diff to previous 90118
Updated Boogie theory.

Revision 90118 - (view) (annotate) - [select for diffs]
Modified Thu Dec 6 16:31:22 2012 UTC (6 years, 10 months ago) by julian
File length: 9229 byte(s)
Diff to previous 90072
Updated Boogie theory.

Revision 90072 - (view) (annotate) - [select for diffs]
Modified Sat Dec 1 15:51:18 2012 UTC (6 years, 10 months ago) by julian
File length: 8110 byte(s)
Diff to previous 89988
Updated Boogie theory.

Revision 89988 - (view) (annotate) - [select for diffs]
Modified Wed Nov 28 13:41:57 2012 UTC (6 years, 10 months ago) by julian
File length: 6536 byte(s)
Diff to previous 89621
Added skeleton for multi-line error reporting in AutoProof.

Revision 89621 - (view) (annotate) - [select for diffs]
Modified Fri Oct 19 12:39:47 2012 UTC (7 years ago) by julian
File length: 5673 byte(s)
Diff to previous 88710
Initial support for reals added to AutoProof.

Revision 88710 - (view) (annotate) - [select for diffs]
Added Thu May 10 14:58:31 2012 UTC (7 years, 5 months ago) by julian
File length: 4706 byte(s)
Added new AutoProof version with translation to intermediate verification AST for translation to Boogie.


This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.23