:PROPERTIES:
:ID: 615071c0-96ea-46d2-a563-87555a3e1640
:mtime: 20240304012202 20240208090544 20240207063818 20240205115303 20240203075837 20240201084625
:ctime: 20240201084622
:END:
#+title: Machine Learning Invariant Project
#+filetags: :workproject:public:project:
* Reading to Do
- Linear Disjunctive Invariant Generation with Farkas’ Lemma : https://jhc.sjtu.edu.cn/~hongfeifu/manuscripta.pdf
- Linear Invariant Generation Using Non-Linear
Constraint Solving : https://www.cs.utexas.edu/~tdillig/cs395/non-linear.pdf
- Total Correctness
- Partial Correctness
* Examples
- https://cs.stackexchange.com/questions/119494/how-to-find-the-loop-invariant-in-hoare-triples
#+BEGIN_SRC python
# PRECONDITION: x > 1 and y > 1
while x > 0:
x = x - 1
y = y + 2 # INVARIANT: 2 * x + y > 5
# POSTCONDITION: x + y > 5
#+END_SRC
#+BEGIN_SRC python
def maximum(a):
# PRECONDITION: a is a non-empty array of positive integers
i = 0
m = 0
while i < len(a):
if m < a[i]:
m = a[i] # INVARIANT: if j <= i, then a[j] <= m
i += 1
# POSTCONDITION: m is the maximum value of a
#+END_SRC
#+BEGIN_SRC python
# PRECONDITION: i + j = 10
while i < 10:
j -= 1
i += 1 # INVARIANT: i + j = 10
# POSTCONDITION: i >= 10 and j <= 0
#+END_SRC python
* Proof of an Example
I will now prove the following:
#+BEGIN_SRC python
# PRECONDITION: x > 1 and y > 1
while x > 0:
x = x - 1
y = y + 2 # INVARIANT: 2 * x + y > 5
# POSTCONDITION: x + y > 5
#+END_SRC
I will prove the invariant inductively.
The base case of the invariant is that we have $x > 1$ and $y > 1$. Thus,
$2 * (x - 1) + (y + 2) = 2 * x - 2 + y + 2 = 2 * x + y > 5$.
In the inductive step, assume that $2 * x + y > 5$. Then,
$2 * (x - 1) + (y + 2) = 2 * x + y > 5$. This proves that the invariant
holds inductively on each iteration of the loop.
Now, we will show that the loop invariant and the negation of the loop condition
$x <= 0$ implies the post-condition.
$x + y >= 2 * x + y > 5$. Thus, we have proven the post-condition.