-
Notifications
You must be signed in to change notification settings - Fork 6
-
Notifications
You must be signed in to change notification settings - Fork 6
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Mapping values of two scalar types #907
Comments
FWIW, the list comprehension syntax does not match that provided by Ada 2022 "filters" -- filters use "when M.Alg = Request_Alg" rather than "if ...", hence "[for M in Maps when M.Alg = Request.Alg => M];" This also might not produce exactly one result. The "dedicated mapping type" could use Ada 2022 syntax for container aggregates (these use "[...]" rather than "(...)") and Ada 2012 syntax for indexing and be supported by SPARK directly. Not sure what you mean by "reusability" concerns. A simple array aggregate would seem to be the simplest, however, in that that provides totality and efficiency. |
@sttaft Thanks for your input!
We actually changed syntax for list comprehensions in the meantime to be more consistent to Ada 2022 (cf. #702), although we decided to still deviate by using the
The concern is that we are adding this new language construct just for this very specific issue. I think newly added feature should ideally cover multiple use cases.
Do you propose adding an array type similar to Ada? That is not yet part of the language, but we could certainly consider it as an option. |
Context and Problem Statement
In protocols the values of two scalar types sometimes have to be mapped onto / converted into each other in a way that cannot be done by a calculation. The most prominent example are algorithms selected in a protocol session which result in response messages of different lengths:
Use Cases
DIGESTS
response based on selected hash algorithm in SPDM protocol (7.4)Considered Options
O1
Use states to select the corresponding value:
+ No changes required
− Very verbose
− Potentially many additional states
− Totality not enforced
O2
Use sequences and list comprehension:
+ No changes required
− Convoluted syntax
− Inefficient code (space and time)
− Intent is not conveyed clearly in specification
− Totality not enforced
O3
Introduce
case
expression:+ Concise
+ Conveys the intent clearly
+ Totality can be enforced
+ Probably easy to transform to SPARK
− Somewhat redundant to existing state transitions
− Inefficient when same mapping is required in multiple places
− Reusability questionable
O4
Use external function:
+ Concise
+ No changes required
− Intent is not conveyed in specification at all
− Totality not enforced
− Code changes may break specification
− Proof may become hard or impossible
O5
Introduce a dedicated mapping type (concrete syntax to be defined):
+ Concise
+ Intent conveyed clearly
+ Potentially easy to translate into SPARK (using arrays)
+ Totality can be enforced
+ Efficient
− Reusability questionable
O6
Introduce expression functions and case expressions:
+ Concise
+ Intent conveyed clearly
+ Totality can be enforced
+ Efficient
+ Reusable
+ Expressive
− May be overkill for problem to solve
O7a
Introduce a dedicated mapping type:
O7b
Introduce a dedicated mapping type:
+ Concise
+ Intent conveyed clearly
+ Potentially easy to translate into SPARK (using arrays)
+ Totality can be enforced
+ Efficient
− Not reusable
− Unusual syntax
− Two new keywords for one new feature
Decision Outcome
O6
The text was updated successfully, but these errors were encountered: