Skip to:

  1. Skip to Jira Navigation
  2. Skip to Side Navigation
  3. Skip to Main Content

PROBPLUGIN Theory Support Bug for Parameters

Description

Hi,

I encountered what I think is a bug in ProB’s treatment of Theory parameters. I am using the nightly build.

Here is my Context. Note that I use two different Sequences, with different values for the type parameter T.

Here is the translated version. There seem to be two issues:

  • the parameter T is not typed

  • the same identifier T is used for both instances of the Sequence data type

When loading in Rodin or Tcl/Tk I get error message (T cannot be found; see below).

Environment

None

Attachments

3

Gliffy Diagrams

Activity

Show:

Jenkins Build Server February 4, 2014 at 5:55 PM

SUCCESS: Integrated in

ProB_Tests_Gradle #13
PROBPLUGIN-92: Added test cases (plagge: rev 1300)

  • /public_examples/EventBPrologPackages/Theory/RecOpTypeRefTest.zip

  • /public_examples/EventBPrologPackages/Theory/RecOpTypeTest.eventb

Jenkins Build Server January 31, 2014 at 1:17 PM

SUCCESS: Integrated in

ProB_Tests_Linux32 #933
PROBPLUGIN-92: Bugfix for recursive operators by introducing a LET similar to direct definitions (plagge: rev 1e9e68f01f1477dc6564767ad0224f5f6b937955)

  • src/bmachine_eventb.pl
    PROBPLUGIN-92: Added test case for recursive operators (plagge: rev 37397539480ae078b256b06662080e35908e9035)

  • src/testcases.pl
    PROBPLUGIN-92: Added test cases (plagge: rev 1300)

  • /public_examples/EventBPrologPackages/Theory/RecOpTypeRefTest.zip

  • /public_examples/EventBPrologPackages/Theory/RecOpTypeTest.eventb

Jenkins Build Server January 31, 2014 at 11:33 AM

SUCCESS: Integrated in

ProB_Tests_Linux64 #7764
PROBPLUGIN-92: Added test case for recursive operators (plagge: rev 37397539480ae078b256b06662080e35908e9035)

  • src/testcases.pl
    PROBPLUGIN-92: Added test cases (plagge: rev 1300)

  • /public_examples/EventBPrologPackages/Theory/RecOpTypeRefTest.zip

  • /public_examples/EventBPrologPackages/Theory/RecOpTypeTest.eventb

Jenkins Build Server January 31, 2014 at 11:01 AM

SUCCESS: Integrated in

ProB_Tests_Linux64 #7763
PROBPLUGIN-92: Bugfix for recursive operators by introducing a LET similar to direct definitions (plagge: rev 1e9e68f01f1477dc6564767ad0224f5f6b937955)

  • src/bmachine_eventb.pl

Daniel Plagge January 31, 2014 at 10:36 AM

Now recursive operators are fixed, too.

Fixed

Details

Assignee

Reporter

Priority

Created January 19, 2014 at 10:55 AM
Updated February 4, 2014 at 5:55 PM
Resolved January 31, 2014 at 10:36 AM
Configure