Form to evaluation of categorization model

This form was created to evaluate the categorization model developed by the researchers Alysson Milanez, Tiago Massoni, and Rohit Gheyi.

The evaluation will be based on answers to this form in comparison with our results.

If you have some question about this form, please send an email to alyssonfilgueira@gmail.com

    The categorization model proposed

    In our study we proposed and implemented a categorization model to nonconformances between code and specification. The model is composed by three-levels: category, type and likely cause. Concerning about categories, an error that apparently occurs in the contract is regarded as specification error; in contrast, apparent error in the body of the problematic method(s) is a code error; it is undefined when it is not possible - considering a non-expert in the application domain - to determine whether the problem is in the contract or in the source code. The type is given automatically by the assertion checker, and corresponds to the part of JML that was violated - considering only visible behavior from the systems. Each error may present several likely causes, which cannot be deterministically diagnosed - debugging can be aided, however, by specific heuristics. In Figure 1 we present an overview of our categorization model.

    Figure 1. Categorization model - overview

    Captionless Image

    Evaluation

    Now we present a list of 10 nonconformances randomly selected from the nonconformances that we detect using JMLOK tool into a set of JML programs. The nonconformances were selected using the sample command from R language (version 3.0.1). The set of JML programs is composed by sample programs available at: http://www.eecs.ucf.edu/~leavens/JML/examples.shtml and six Open-source JML programs: Bomber, HealthCard, JAccounting, JSpider, Mondex and TransactedMemory. While Bomber is a mobile game, HealthCard is an application that manages medical appointments into smart cards. JAccounting and JSpider are two case studies from the ajml compiler project, implementing, respectively, an accounting system and a Web Spider Engine. Mondex is a system whose translation from original Z specification was developed in the Verified Software Repository context. Finally, TransactedMemory is a specific feature of the Javacard API. First we present the methodology to be used to categorize nonconformances. Then we present some details about each nonconformance, like location and type. Next we show a test case that reveals the nonconformance. Finally, we present the source code and specification related to the nonconformance.

    Methodology to categorize

    1. Examining the project domain where the nonconformance was detected. 2. Examining test case that reveals the nonconformance. a. Understanding the modifications into the object under test until the nonconformance be revealed. 3. Examining source code and specification. 4. Choosing a category between: code, specification, or undefined. 5. Suggesting a likely cause for the nonconformance.

    Experimental Unit - Samples

    Nonconformance details

    Source code: https://www.dropbox.com/sh/0bv6vu7z74anobw/vy4lIZY-MV Package: BoundedStack Class: BoundedStack Method: Constructor - BoundedStack Type: postcondition

    Test case that reveals this nonconformance:

    Captionless Image
    This is a required question
    Must be at least 1 characters.
    This is a required question

    Nonconformance details

    Source code: https://www.dropbox.com/sh/srg8y8fgy0037no/GmCdQ8mUWi Package: stacks Class: BoundedStack Method: Constructor - BoundedStack Type: invariant

    Test case that reveals this nonconformance:

    Captionless Image
    This is a required question
    Must be at least 1 characters.
    This is a required question

    Nonconformance details

    Source code: https://www.dropbox.com/sh/z4l0yd3g9tdu9iw/Xs0L29FYDY Package: dbc Class: Rectangular Method: imaginaryPart Type: postcondition

    Test case that reveals the nonconformance:

    Captionless Image
    This is a required question
    Must be at least 1 characters.
    This is a required question

    Nonconformance details

    Source code: https://www.dropbox.com/sh/h7ulctxpzhkxjkk/ITYh5NImNv Package: list Subpackage: list3 Class: TwoWayIterator Method: next Type: postcondition

    Test case that reveals this nonconformance

    Captionless Image
    This is a required question
    Must be at least 1 characters.
    This is a required question

    Experimental Unit - HealthCard

    Nonconformance details

    Source code: https://www.dropbox.com/sh/9ljqnakvx35x93u/PlGyTp_vk9 Package: allergies Class: Allergies_Impl Method: setAllergyDesignation Type: postcondition

    Test case that reveals this nonconformance

    Captionless Image
    This is a required question
    Must be at least 1 characters.
    This is a required question

    Nonconformance details

    Source code: https://www.dropbox.com/sh/rwma5927f1qfkmp/rrQV6oWrdl Package: treatments Class: Treatment_Impl Method: setTreatmentID Type: invariant

    Test case that reveals this nonconformance:

    Captionless Image
    This is a required question
    Must be at least 1 characters.
    This is a required question

    Nonconformance details

    Source code: https://www.dropbox.com/sh/g4fgnapwtdhdip6/aQwWNmqBQ7 Package: vaccines Class: Vaccine_Impl Method: setDesignation Type: precondition

    Test case that reveals this nonconformance:

    Captionless Image
    This is a required question
    Must be at least 1 characters.
    This is a required question

    Nonconformance details

    Source code: https://www.dropbox.com/sh/g4fgnapwtdhdip6/aQwWNmqBQ7 Package: vaccines Class: Vaccines_Impl Method: getVaccineDesignation Type: postcondition

    Test case that reveals this nonconformance:

    Captionless Image
    This is a required question
    Must be at least 1 characters.
    This is a required question

    Experimental Unit - JAccounting

    Nonconformance details

    Source code: https://www.dropbox.com/sh/879pkt9pwedkh49/g83IEk-3d_ Package: com.spaceprogram Subpackage: util Class: ArrayUtils Method: getMaxIntArrayIndex Type: postcondition

    Test case that reveals this nonconformance:

    Captionless Image
    This is a required question
    Must be at least 1 characters.
    This is a required question

    Nonconformance details

    Source code: https://www.dropbox.com/sh/879pkt9pwedkh49/g83IEk-3d_ Package: com.spaceprogram Subpackage: util Class: CookieUtils Method: getDeleteCookie Type: postcondition

    Test case that reveals this nonconformance:

    Captionless Image
    This is a required question
    Must be at least 1 characters.
    This is a required question