tnelson / Forge

Forge: A Tool and Language for Teaching Formal Methods
https://forge-fm.org/
MIT License
67 stars 9 forks source link

Partial-instance sugar in Froglet #215

Closed tnelson closed 9 months ago

tnelson commented 1 year ago

The partial-instance syntax of Froglet has some leaky abstraction. E.g.,

board = Board -> (1 -> 1 -> `X + 1 -> 2 -> `O)

There are two issues here. (1) The definition of fields uses relational syntax. (2) Board must be defined in the partial instance before it can be used, even if its scope will be provided numerically.

Proposed alternative syntax for (1) :

Board0.board = (1, 1) -> `X ;
                            (1, 2) -> `O ; 

Edit: this also applies to field definitions.

tnelson commented 10 months ago

217 addresses (1) but not (2). The syntax does not include semicolons, since it is often used in modeling languages to represent sequential composition. Instead, + is used.