/[eiffelstudio]/trunk/research
ViewVC logotype

Log of /trunk/research

View Directory Listing Directory Listing


Sticky Revision:

Revision 103717 - Directory Listing
Modified Sun Dec 8 19:21:13 2019 UTC (3 days, 23 hours ago) by alexk
Fixed a typo in a message.

Revision 103503 - Directory Listing
Modified Wed Sep 11 14:53:11 2019 UTC (3 months ago) by alexk
Changed the order of initializing a context for an expression translator and setting associated mapping, so that supplied mapping is set after initializing context with default "Current".
Fixed spelling mistakes.


Revision 103502 - Directory Listing
Modified Wed Sep 11 14:50:07 2019 UTC (3 months ago) by alexk
Fixed a bug introduced when typing Current for MML classes by updating Current expression only when it is an entity (i.e., not a more complex expression) and has a type different from the specified context type.

Revision 103501 - Directory Listing
Modified Tue Sep 10 19:07:57 2019 UTC (3 months ago) by alexk
Corrected translation of object tests inside routine body to generate and use a temporary variable for an object test local (this fixes verification of routines that use object test locals for wrapping/unwrapping).

Revision 103500 - Directory Listing
Modified Tue Sep 10 18:30:05 2019 UTC (3 months ago) by alexk
Removed assertions that are no longer needed for verification.

Revision 103499 - Directory Listing
Modified Tue Sep 10 13:55:54 2019 UTC (3 months ago) by alexk
Added a clause telling that `observers` do not change after a call to `lock`.

Revision 103498 - Directory Listing
Modified Tue Sep 10 13:53:27 2019 UTC (3 months ago) by alexk
Removed class status of feature `observers` because it is object-relative.
Marked `set_observers` as a ghost feature.
Added a postcondition to the feature `set_observers` to specify that `observers` is set to the specified value after the call to it.
Generalized implementation of the guard feature `in_observers` to handle the case when type of `observers` is changed in descendants.


Revision 103497 - Directory Listing
Modified Tue Sep 10 13:31:39 2019 UTC (3 months ago) by alexk
Ignored an automatically generated file.

Revision 103496 - Directory Listing
Modified Tue Sep 10 13:29:59 2019 UTC (3 months ago) by alexk
Corrected `set_context` to set `origin_class` using byte context data because it can be different from the current type.

Revision 103495 - Directory Listing
Modified Tue Sep 10 13:28:42 2019 UTC (3 months ago) by alexk
Corrected the way how typing context is handled by features `translate_inline_invaraint_check` and `process_immediate_invariants`: now it is set at the beginnig of the features and restored to the original state at the end. Together with the following commit, it makes sure all classes of "base2" and "mml" librares can be successfully verified.
Made sure typing context is properly set at the beginning of `translate_invariant`.


Revision 103494 - Directory Listing
Modified Tue Sep 10 13:16:22 2019 UTC (3 months ago) by alexk
Made sure the guard feature type is computed against the type where it is checked, not where it is originally written to avoid the case when the guard feature depends on a formal generic through an acnhored type, and there is no formal generic in the class where the feature is written.

Revision 103493 - Directory Listing
Modified Tue Sep 10 13:10:10 2019 UTC (3 months ago) by alexk
Added features to switch context type in a stack-like manner to restore the context after processing inherited or/and inlined features.

Revision 103491 - Directory Listing
Modified Sat Sep 7 08:36:49 2019 UTC (3 months ago) by alexk
Updated to the most recent version of ECF schema to use new defaults.
Requested to report warnings as errors.


Revision 103490 - Directory Listing
Modified Sat Sep 7 08:35:36 2019 UTC (3 months ago) by alexk
Fixed a bug that could lead to skipping verification of some features of a class to be verified or out-of-bound access caused by the iteration on a container that can be updated at every cycle.

Revision 103489 - Directory Listing
Modified Sat Sep 7 08:30:37 2019 UTC (3 months ago) by alexk
Taken current class into account when translating Current to handle built-in features as expected so that lemmas of MML classes can be verified.
Used 8-bit strings compiler features instead of 32-bit ones to avoid unnecessary conversion.
Used READABLE_STRING instead of STRING to avoid conversion.
Replaced reverse assignments with object tests.


Revision 103464 - Directory Listing
Modified Wed Sep 4 07:08:48 2019 UTC (3 months, 1 week ago) by alexk
Fixed implementation of `same_expression` that was checking whether the other expression is of type `IV_FORALL` rather than `IV_EXISTS`.

Revision 103463 - Directory Listing
Modified Wed Sep 4 07:06:27 2019 UTC (3 months, 1 week ago) by alexk
Supported reading of execution time that was formatted with a comma instead of a dot and avoided assertion violation when the time is not in the expected format.

Revision 103462 - Directory Listing
Modified Wed Sep 4 06:58:14 2019 UTC (3 months, 1 week ago) by alexk
Enabled assertions.

Revision 103456 - Directory Listing
Modified Mon Sep 2 19:26:05 2019 UTC (3 months, 1 week ago) by alexk
Changed ECF schema version to use recent defaults.
Requested to report warnings as errors.


Revision 103455 - Directory Listing
Modified Mon Sep 2 19:24:59 2019 UTC (3 months, 1 week ago) by alexk
Replaced reverse assignments with object tests.

Revision 103453 - Directory Listing
Modified Mon Sep 2 18:35:23 2019 UTC (3 months, 1 week ago) by alexk
Changed feature signatures to avoid calls to obsolete feature `as_string_8`.

Revision 103452 - Directory Listing
Modified Mon Sep 2 13:19:54 2019 UTC (3 months, 1 week ago) by alexk
Updated to the most recent version of ECF schema to use new defaults.

Revision 103247 - Directory Listing
Modified Fri May 31 07:32:21 2019 UTC (6 months, 1 week ago) by alexk
Changed ECF schema version to use recent defaults.

Revision 103246 - Directory Listing
Modified Fri May 31 07:30:28 2019 UTC (6 months, 1 week ago) by alexk
Supported file names in Unicode.
Replaced arrays with arrayed lists to avoid using obsolete features and to move towards void safety.
Used standard classes instead of those from Gobo.
Replaced reverse assignments with object tests.
Relied on standard layout to lookup files.
Replaced standard loops with ITERABLE-based ones.
Added error reporting when some required features are not found in the standard classes.
Added PREDICATE to the list of known agent types.


Revision 103245 - Directory Listing
Modified Fri May 31 07:11:59 2019 UTC (6 months, 1 week ago) by alexk
Removed unused local variables.

Revision 103244 - Directory Listing
Modified Fri May 31 07:07:26 2019 UTC (6 months, 1 week ago) by alexk
Added a feature to check whether a 32-bit string is a valid name.

Revision 103243 - Directory Listing
Modified Fri May 31 07:05:50 2019 UTC (6 months, 1 week ago) by alexk
Removed an empty description.

Revision 103242 - Directory Listing
Modified Fri May 31 07:04:56 2019 UTC (6 months, 1 week ago) by alexk
Replaced a comparison against a manifest constant with a specific query

Revision 103241 - Directory Listing
Modified Fri May 31 07:03:46 2019 UTC (6 months, 1 week ago) by alexk
Enabled warnings.

Revision 103240 - Directory Listing
Modified Fri May 31 07:00:25 2019 UTC (6 months, 1 week ago) by alexk
Removed an empty argument list.

Revision 102682 - Directory Listing
Modified Fri Dec 28 21:18:39 2018 UTC (11 months, 2 weeks ago) by alexk
Changed formal generic constraints to be non-separate because separate items could be changed by some other processor and break properties of containers relying on items state.

Revision 102681 - Directory Listing
Modified Fri Dec 28 21:14:17 2018 UTC (11 months, 2 weeks ago) by alexk
Moved modify clauses to postconditions.

Revision 102680 - Directory Listing
Modified Fri Dec 28 21:13:20 2018 UTC (11 months, 2 weeks ago) by alexk
Added a configuration file to compile the library in SCOOP mode.

Revision 102672 - Directory Listing
Modified Sat Dec 22 10:51:03 2018 UTC (11 months, 2 weeks ago) by alexk
Moved modify clauses to postconditions.

Revision 102671 - Directory Listing
Modified Sat Dec 22 10:32:04 2018 UTC (11 months, 2 weeks ago) by alexk
Removed redefinitions that violate VDRS(4) when a deferred feature is effected in the class, not redefined.

Revision 102670 - Directory Listing
Modified Sat Dec 22 10:20:00 2018 UTC (11 months, 2 weeks ago) by alexk
Removed redefinitions that violate VDRS(4) when a deferred feature is effected in the class, not redefined.

Revision 102523 - Directory Listing
Modified Fri Nov 23 13:12:53 2018 UTC (12 months, 2 weeks ago) by alexk
Supported built-in conversion of basic types.

Revision 102522 - Directory Listing
Modified Fri Nov 23 12:43:57 2018 UTC (12 months, 2 weeks ago) by alexk
Added protection for the case when MML_SET is not available.

Revision 102418 - Directory Listing
Modified Mon Nov 12 10:44:25 2018 UTC (12 months, 4 weeks ago) by alexk
Made feature `FIBONACCI.new_cursor` non-class to support current implementation of observers.

Revision 102417 - Directory Listing
Modified Mon Nov 12 09:40:43 2018 UTC (12 months, 4 weeks ago) by alexk
Moved modify clause to postcondition.

Revision 102353 - Directory Listing
Modified Sun Oct 21 14:53:13 2018 UTC (13 months, 3 weeks ago) by alexk
Made feature `PRIMES.new_cursor` non-class to support current implementation of observers.

Revision 102187 - Directory Listing
Modified Mon Sep 17 12:01:15 2018 UTC (14 months, 3 weeks ago) by alexk
Supported assertion tags with spaces that can be used when there are no explicit assertion tags and the corresponding expressions are used instead.

Revision 102186 - Directory Listing
Modified Mon Sep 17 11:44:09 2018 UTC (14 months, 3 weeks ago) by alexk
Added missing message formatting.

Revision 102185 - Directory Listing
Modified Mon Sep 17 11:40:22 2018 UTC (14 months, 3 weeks ago) by alexk
Used case-insensitive comparison when comparing with `assume`.

Revision 102164 - Directory Listing
Modified Thu Sep 13 16:59:10 2018 UTC (14 months, 4 weeks ago) by alexk
Moved modify clauses to postconditions.

Revision 102163 - Directory Listing
Modified Thu Sep 13 16:52:12 2018 UTC (14 months, 4 weeks ago) by alexk
Changed processing of modify clauses to have them in postconditions.

Revision 102115 - Directory Listing
Modified Fri Aug 31 14:24:38 2018 UTC (15 months, 1 week ago) by alexk
Made code completely void-safe except for features {V_HASH_TABLE}.make, {V_DOUBLY_LINKABLE}.insert_right, {V_DOUBLY_LINKABLE}.remove_right by
	- using design mode for ghost functions returning non-void reference values;
	- initializing local variables referencing ghost state;
	- adding attachment marks;
	- adding formal generic constraints;
	- adding object tests and checks for False when attachment status of an expression is known to the verifier;
	- adding additional checks before object tests so that they are handled by the verifier as expected.
Removed conversion function {TUPLE}.to_mml_set because it does not work well when attachment marks of actual generics of MML_SETs used in comparison or reattachment are different.
Added an ECF (base-safe.ecf) for a version of the base library excluding classes that are not completely void-safe or depend on them:
	- V_DOUBLY_LINKABLE
	- V_DOUBLY_LINKED_LIST
	- V_DOUBLY_LINKED_LIST_ITERATOR
	- V_HASH_SET
	- V_HASH_SET_ITERATOR
	- V_HASH_TABLE
	- V_HASH_TABLE_ITERATOR


Revision 102108 - Directory Listing
Modified Fri Aug 31 11:03:33 2018 UTC (15 months, 1 week ago) by alexk
Added initialization of `internal_last_string_`.

Revision 102107 - Directory Listing
Modified Fri Aug 31 10:57:20 2018 UTC (15 months, 1 week ago) by alexk
Added an explicit type to a manifest integer to make sure verification passes.

Revision 102102 - Directory Listing
Modified Tue Aug 28 19:59:08 2018 UTC (15 months, 2 weeks ago) by alexk
Ignored a compilation directory.

Revision 102101 - Directory Listing
Modified Tue Aug 28 19:57:27 2018 UTC (15 months, 2 weeks ago) by alexk
Updated to be compatible with full class checking.

Revision 102100 - Directory Listing
Modified Tue Aug 28 19:00:17 2018 UTC (15 months, 2 weeks ago) by alexk
Cosmetics: removed an unnecessary white space character.

Revision 102099 - Directory Listing
Modified Tue Aug 28 18:58:20 2018 UTC (15 months, 2 weeks ago) by alexk
Removed unused local variables.

Revision 102098 - Directory Listing
Modified Tue Aug 28 18:20:47 2018 UTC (15 months, 2 weeks ago) by alexk
Adapted EVE version of the base library to be used with the standard version of this library.
Added scripts to automate conversion of base library classes and ECF to autoproof-aware ones.
Adapted MML library for use with the current Eiffel.
Imported base2 library so that it's code can be updated if needed.


Revision 102092 - Directory Listing
Modified Tue Aug 28 10:37:26 2018 UTC (15 months, 2 weeks ago) by jfiat
Fixed signature to avoid potential catcall.

Revision 102069 - Directory Listing
Added Fri Aug 24 18:15:30 2018 UTC (15 months, 2 weeks ago) by alexk
Added a research directory for projects built on top of official EiffelStudio without the need to duplicate code in branches, perform two-way merges and other maintainance activities. The projects should always be kept up-to-date with the rest of the trunk.

  ViewVC Help
Powered by ViewVC 1.1.23