-
Notifications
You must be signed in to change notification settings - Fork 0
/
TODO.txt
50 lines (45 loc) · 2.85 KB
/
TODO.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
Stuff to do:
*** 1. Add openid support for logins
*** 3. Check if social OAuth is possible
4. Remove confirm form resubmission and try to dissociate views from urls if possible
*** 5. Click line number to add invariant
6. User profile page
7.
8.
*** 9. "Forgot password" functionality
*** 10. "Remember me" when signing in
11. Autofill user details in Disqus
*** 12. Add email sending facility (sendgrid)
*** 13. Add auxiliary user database to support more user info
14. Add incentive mechanism - scores for invariants, leaderboards, and user proficiency level
15. What does it mean to say that a program is correct? We're not even passing assertions between programs
16. Exception handling when submitting invariant (parsing or Z3 errors etc. not handled right now)
*** 17. Further refine invariant filter in the results
*** 18. Along with checking variable values in the trace, allow the user to also track values of predicates (both correct and unknown status), just so that the user can realize how predicates are behaving
19. Display partial traces only for programs that are parts of larger programs
20. Display the right line numbers for programs that are parts of larger programs
*** 21. Allow user to give counter examples for unknown invariants (this doesn't help verification)
22. Add migration capability on Heroku
24. Results table should be AJAX
+++ 25. Related to (21), also use the "interesting" inputs that users give to try and refute other facts.
+++ 26. Combine "unknown" loop invariants in the hope that they are auxiliary invariants for each other
27. Should variables be allowed to be used in invariants only if they are defined? This saves us from dealing with trashy invariants
+++ 29. Add a program with if-else statement
+++ 30. Multiple functions?
31. Checkbox to prevent DB additions
+++ 32. Tutorial page.
+++ 33. Only suggest invariants, not loop invariants.
*** = future work
+++ = important
---- Steps when adding a new program to the database ----
1. Create instrumented code
2. Create unix binary
3. Create Z3Program child class for the program
4. Add symbol table
5. Add entry in Z3ProgramFactory
6. Add cleaned up code and meta to the static/code folder
7. Enter in database
---- Discussion (4/9/13) ----
1. If A and B by themselves are unknown invariants on their own, A^B may turn out to be a correct invariant. The backend should occasionally combine all the "unknown" invariants and check them together, drop some, fork, check, drop, etc.
2. Code division: Just display chunks, but invariants are always attached to the parent program
Possible solution for 19,20 (as discussed before also, but writing here just for the record): There is only one program, even if it is ever divided up. We only choose what lines of it to display upon any program page on the front end. Facts that are entered for parts are of course proved modulo known facts for the entire program