Project

General

Profile

Feature #2290

[Analysis] Components should be considered as black box by default if they are not implemented

Added by Anonymous over 5 years ago. Updated about 1 year ago.

Status:
Rejected
Priority:
Normal
Assignee:
-
Category:
-
Target version:
Start date:
02/06/2015
Due date:
% Done:

0%

Estimated time:

History

#1 Updated by Anonymous about 5 years ago

  • Target version changed from AF3 2.8 RC1 (Feature Freeze) to AF3 2.9 RC1 (Features frozen)

#2 Updated by Anonymous over 4 years ago

  • Target version changed from AF3 2.9 RC1 (Features frozen) to AF3 2.10 Feature Freeze

#3 Updated by Anonymous about 4 years ago

  • Target version changed from AF3 2.10 Feature Freeze to AF3 2.11 RC1 (Feature Freeze)

#4 Updated by Anonymous over 3 years ago

  • Target version changed from AF3 2.11 RC1 (Feature Freeze) to AF3 2.11 Post-release

#5 Updated by Anonymous almost 3 years ago

  • Assignee changed from Anonymous to Anonymous
  • Target version changed from AF3 2.11 Post-release to AF3 2.13 RC1 (Feature Freeze)

@Sudeep: this should be essentially done in the transformation: if a component does not contain any behavior then we make use of a default contract "Assume TRUE Guarantee TRUE".

What do you say? Probably low priority right?

#6 Updated by Anonymous almost 3 years ago

Yes. Low priority.

We do not need to generate the default contract. User can specify contracts on the empty components and then these can be used for refinement verification. Status should be "NOT VERIFIED" or "NOT APPLICABLE", and verification of these contracts against implementation should not be triggered.

#7 Updated by Anonymous over 2 years ago

  • Target version changed from AF3 2.13 RC1 (Feature Freeze) to AF3 2.14 RC1 (Feature Freeze)

#8 Updated by Anonymous over 1 year ago

  • Assignee changed from Anonymous to Anonymous

It is not clear what is expected to be done.

The current status is - We are able to define the contracts on an empty component. They are verified against an empty state machine. So, as a result some of them pass and some of them fail.

I don't see it as such a big problem. If you are not satisfied with the current state, please describe the expected behaviour more clearly.

Either close the issue or clarify.

#9 Updated by Johannes Eder over 1 year ago

  • Target version changed from AF3 2.14 RC1 (Feature Freeze) to Backlog

#10 Updated by Anonymous about 1 year ago

  • Assignee changed from Anonymous to Johannes Eder

It can be rejected

#11 Updated by Johannes Eder about 1 year ago

  • Status changed from New to Rejected
  • Assignee deleted (Johannes Eder)

Also available in: Atom PDF