Procedure parameter modes (in .rb files) must match corresponding Operation parameter modes (in .co files) - Githubissues

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

Procedure parameter modes (in .rb files) must match corresponding Operation parameter modes (in .co files) #12

Open drholly77 opened 1 month ago

drholly77 commented 1 month ago

Context:

The operation headers found in a concept file (extension .co) start with the keyword Operation
The corresponding headers in the realization file (extension .rb) starts with the keyword Procedure
The .rb file is always located in the same directory as its corresponding .co file

To be checked:

Each parameter mode found in a Procedure header must exactly match the corresponding parameter mode found the Operation header, with the following exceptions:

If alters appears in the Operation header, then either alters or clears can appear in the corresponding Procedure header
If restores appears in the Operation header, then either restores or preserves can appear in the corresponding Procedure header

Compiler error:

Generate a compiler error message if this check fails

Note:

.rb files may contain additional Procedures that are not defined in the .co