search

mbeddr / language_verification

A collection of tools and technologies for verifying software languages developed using JetBrains' MPS.
Other
1 stars 0 forks source link

Different backward link semantics #4

Open levilucio opened 8 years ago

levilucio commented 8 years ago

Backward link semantics:

Semantics 1 (Implemented): precondition only matches over elements from the match part of the part of the path condition. postcondition matches over traceability links plus apply part of the path condition.

Semantics 2 (NOT Implemented): precondition over elements from the match part of the path condition and traceability. Postcondition matches the rest.

Both semantics are needed, they mean different things. Can be implemented as a flag on backward links to signal individual backward link semantics. The isolated, connected and complete matchers need to be changed accordingly.

levilucio commented 8 years ago

@BentleyJOakes Can you close if all is done?