This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
bpmn-leaks-when-analysis [2019/10/01 13:53] 127.0.0.1 external edit |
bpmn-leaks-when-analysis [2020/01/23 12:30] pullonen |
||
---|---|---|---|
Line 14: | Line 14: | ||
The source code of the analysis tool is available at [[https://github.com/pleak-tools/pleak-leaks-when-analysis|pleak-leaks-when-analysis]] repository. The user interface of the analysis tool is accessible through [[https://github.com/pleak-tools/pleak-sql-editor|pleak-sql-editor]]. | The source code of the analysis tool is available at [[https://github.com/pleak-tools/pleak-leaks-when-analysis|pleak-leaks-when-analysis]] repository. The user interface of the analysis tool is accessible through [[https://github.com/pleak-tools/pleak-sql-editor|pleak-sql-editor]]. | ||
+ | |||
+ | ===== Syntax ===== | ||
+ | |||
+ | Association lists are a GADT "(keytype * valuetype) assoclist" with the following six operations: | ||
+ | |||
+ | nil : (keytype * valuetype) assoclist | ||
+ | add_data_to_store : keytype -> valuetype -> (keytype * valuetype) assoclist -> (keytype * valuetype) assoclist | ||
+ | update : keytype -> valuetype -> (keytype * valuetype) assoclist -> (keytype * valuetype) assoclist | ||
+ | find : keytype -> (keytype * valuetype) assoclist -> valuetype | ||
+ | endsWith : keytype -> (keytype * valuetype) assoclist -> bool /* note that this probably used in the opposite direction in the model */ | ||
+ | contains : keytype -> (keytype * valuetype) assoclist -> bool | ||
+ | |||
+ | They satisfy the following equalities: | ||
+ | |||
+ | endsWith(, nil) = false | ||
+ | contains(, nil) = false | ||
+ | endsWith(K, add(K', , L)) = (K == K') | ||
+ | endsWith(K, update(, _, L)) = endsWith(K, L) | ||
+ | contains(K, add(K', , L)) = (K == K') || contains(K, L) | ||
+ | contains(K, update(, , L)) = contains(K, L) | ||
+ | find(, nil) = bottom | ||
+ | find(K, add(K', V, L)) = if K == K' then V else find(K, L) | ||
+ | find(K, update(K', V, L)) = if contains(K, L) then (if K = K' then V else find(K, L)) else bottom |