rhit-csse-projects / RESOLVE

RESOLVE (REusable SOftware Language with VErification) is a specification and programming language designed for verifying correctness of object oriented programs.
https://www.cs.clemson.edu/resolve/
BSD 3-Clause "New" or "Revised" License
0 stars 0 forks source link

Easy: Concept parameter mode usage checking (10 hrs) #2

Open AdityaSenthilvel opened 2 months ago

AdityaSenthilvel commented 2 months ago

Check misuse of # notation in the ensures clause wrt parameter mode. These may be warnings as opposed to errors.

drholly77 commented 2 months ago

@rhit-csse-projects/t17-2425 Suppose there is a parameter X When to issue a warning by different parameter modes:

  1. restores X or preserves X or evaluates X: issue a warning if the ensures clause includes a #X
  2. replaces X: issue a warning if there is a #X in the ensures clause
  3. alters X: issue a warning if there is an X (i.e., w/o the #) in the ensures clause
  4. updates X or clears X: issue no warnings for these modes

Explanation:

  1. These parameter modes all mean that X = #X, i.e., the outgoing X is equal to the incoming X
  2. The replaces mode means that the operation ignores the incoming value
  3. The alters mode means that the outgoing value is unspecified
rhit-koenigjl commented 2 months ago

Useful Classes: