/[eiffelstudio]
ViewVC logotype

Revision 95474


Jump to revision: Previous Next
Author: polikarn
Date: Tue Jul 22 08:59:37 2014 UTC (5 years, 1 month ago)
Changed paths: 19
Log Message:
Simplified partial contracts. Introducing extra bound vars to replace arithmetic in quantifiers (alternative to triggering on arithmetic).

Changed paths

Path Details
Directorybranches/eth/eve/Src/Eiffel/interface/graphical/tools/autoproof/es_autoproof_tool_panel.e modified , text changed
Directorybranches/eth/eve/Src/Eiffel/interface/tty/ewb_boogie_verification.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/iv/iv_binary_operation.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/iv/iv_conditional_expression.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/iv/iv_entity.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/iv/iv_expression.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/iv/iv_factory.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/iv/iv_function_call.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/iv/iv_map_access.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/iv/iv_map_update.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/iv/iv_quantifier.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/iv/iv_unary_operation.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/iv/iv_value.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/advanced/partial/a_partial.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/tests/comcom/lcp/longest_common_prefix.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/across/e2b_interval_across_handler.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_instruction_translator.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_options.e modified , text changed
Directorybranches/eth/eve/Src/framework/eiffel2boogie/translation/e2b_routine_translator.e modified , text changed

  ViewVC Help
Powered by ViewVC 1.1.23