search

acsl-language / acsl

Sources for the ANSI/ISO C Specification Language manual
Other
49 stars 8 forks source link

pure C functions used as logical functions #32

Open davidcok opened 6 years ago

davidcok commented 6 years ago

This is a place holder for a issue with many ramiifications. Like in JML and likely in ACSL++, it would be useful to allow pure C functions to be used in logical expressions. This could be accomplished as syntactic sugar -- marking a function pure impliictly creates a corresponding logical function or predicate. I suggest that the marking of pure be required (and then syntactically checked); what the 'corresponding logical function' is requires thought and elaboration.

jensgerlach commented 6 years ago

This might be particularly appealing for ACSL++ where one encounters pure getter methods.

pbaudin commented 6 years ago

Could you tell me if the minimal implicit contact of that pure C function is //@ assigns \nothing ; [ allocates \nothing ; frees \notthing ; ] or something more stronger (note: I put into brackets clauses that can be omitted since that is their default value)?