TODO.txt

New TODO list system:

Important TODOs:
create exceptions
detailed log
invariant boundary testing

create data structures instead of straight string manipulation? New Calculation object or something with C F etc. saved => Fixpoint object, Function object etc.
=> private LinkedHashMap<String,String> fixpointCache = new LinkedHashMap<String,String>(); instead <Fixpoint>

maven build

not only fixpoints as witnesses?

TODO:

remove delta input for evaluation; if hash if defined for all components
fix maven guava dependency
make log appear in runtime => threads? concurrency in swing
write readme with usage and documentation / rename github
write systematic tests
clear cache on restriction/iteration count change (?)

DONE:
create MVC pattern controller!!! DONE
comment all methods and code DONE
persistent file caching of fixpoints to load / save for faster results DONE
hover over buttons for full text in whileLoops DONE
reset Cache button DONE
write tests for all new methods DONE
add license DONE
need to round x1c1? DONE
Implement hash function + iteration DONE
adjust GUI according to hash function calculation DONE
allow witness input and calculation DONE
Question: Dont we need to consider [not guard ] * f in Phi(X) somehow? => we basically test wp hash DONE we consider PHI not wp
DONE while after while all sigma fix
DONE while in while caching
DONE while button list on select highlight selected one, as well as examine button













Obsolete:
First prototype tool that can calculate wp formulas
Results: wp(C)(f)

Inputs:
C Probabilistic Programm
f (post) expectation
k (Co-domain expectations)
m (Co-domain variables)
sigma (Var, initial state) 

Steps:
1. We need a parser  for the formula and evaluation 
(https://mathparser.org/) or check further online
<dependency>
   <groupid>org.mariuszgromada.math</groupid>
   <artifactid>MathParser.org-mXparser</artifactid>
   <version>5.0.2</version>
</dependency>


Output: Stdout (for the beginning)

2. Test formulas from presentation (perhaps limit by boolean 0,1)

3. Call again


BIG TODO:
1) DONE New Sequential System with prior parsing check 
2) New Variable System with persistent variables 
=> fix variable substitution order
=> fix variable flush for testing
=> need more concrete examples for working out the variable assignment problem
3) While Loop implementation 
4) More test cases
5) User Interface implementation


June: 
need to reimplement #{} min operator for proper 0 and k truncation