Differences

This shows you the differences between two versions of the page.

--- bpmn-leaks-when-analysis [2019/09/29 16:53]
admin
+++ 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]].
+===== 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

PLEAK Wiki

User Tools

Site Tools

Differences

Page Tools