formal verification in R?
Does anyone know of work applying formal methods to R?
I'm particularly interested in work attempting to formally verify R's machine learning algorithms: when a big ML system generates a counterintuitive answer, what assurances are there that it's correctly implemented the underlying algorithms?
Thank you in advance,
Colin
See also questions close to this topic

R dataframe subtraction resulting in zeros everywhere
Is there something I am missing about R's dataframe operations because the results are unexpected.When subtract two data frames the resulting frame has zeros almost everywhere.
Here I try to get the log returns of the datahead frame with 15 rows and the result has zeros from the 6th row yet this should not be the case.
> datahead<head(data, n=15) > datahead Safcom nse20 nasi coop 11Aug17 24.50 3976.98 165.00 16.15 10Aug17 24.25 3903.29 162.74 15.90 09Aug17 23.75 3850.13 160.54 15.85 07Aug17 23.50 3818.27 158.83 15.70 04Aug17 23.50 3775.89 158.17 15.55 03Aug17 23.75 3773.52 158.94 15.60 02Aug17 24.00 3741.46 158.94 15.65 01Aug17 23.75 3742.50 158.35 15.70 31Jul17 24.50 3797.53 161.35 15.65 28Jul17 24.50 3798.63 161.18 15.40 27Jul17 23.75 3764.74 158.40 15.10 26Jul17 23.75 3768.38 158.35 15.15 25Jul17 23.50 3729.81 157.05 15.00 24Jul17 23.25 3712.13 156.11 15.00 21Jul17 23.25 3700.44 155.30 14.95 > return.datahead<log(datahead[6,]/datahead[1,]) > return.datahead Safcom nse20 nasi coop 11Aug17 0.01025650 0.0187029500 0.013791639 0.015600940 10Aug17 0.02083409 0.0137128733 0.013610703 0.003149609 09Aug17 0.01058211 0.0083094735 0.010708685 0.009508788 07Aug17 0.00000000 0.0111613240 0.004164044 0.009600074 04Aug17 0.01058211 0.0006278637 0.004856369 0.003210276 02Aug17 0.00000000 0.0000000000 0.000000000 0.000000000 01Aug17 0.00000000 0.0000000000 0.000000000 0.000000000 31Jul17 0.00000000 0.0000000000 0.000000000 0.000000000 28Jul17 0.00000000 0.0000000000 0.000000000 0.000000000 27Jul17 0.00000000 0.0000000000 0.000000000 0.000000000 26Jul17 0.00000000 0.0000000000 0.000000000 0.000000000 25Jul17 0.00000000 0.0000000000 0.000000000 0.000000000 24Jul17 0.00000000 0.0000000000 0.000000000 0.000000000 21Jul17 0.00000000 0.0000000000 0.000000000 0.000000000
Please help on what I should do?

How to add inside legend for a combined plot in ggplot2
I have the following df and ggplot2 code to make a scatter plot but failed to add a legend inside the plot. Thanks :)
x1 = 1:5 x2 = 6:10 y1 = 3:7 y2 = 2:6 df < data.frame(x1, y1, x2, y2) ggplot(df) + geom_point(aes(x=x1, y = y1),col='red') + geom_point(aes(x = x2, y = y2),col='black')

How to tell if uniroot.all has failed to find roots
I am running
uniroot.all
from the packagerootSolve
in the following way:All < uniroot.all(fun, c(0, 1))
which for my equation usually gives me two roots:
All [1] 0.1000000 0.9732628
Sometimes there are no roots, but how can I test on the next line in R that that is the outcome? The result is the following:
numeric(0)
is.nan(All) and is.null(All) return FALSE. I tried looking at the man page and didn't see any mention of a flag for whether roots had been found or the number of roots found. I would have expected NULL as the returned value in this case.

From set inclusion to set equality in lean
Given a proof of set inclusion and its converse I'd like to be able to show that two sets are equal.
For example, I know how to prove the following statement, and its converse:
open set universe u variable elem_type : Type u variable A : set elem_type variable B : set elem_type def set_deMorgan_incl : A ∩ B ⊆ set.compl ((set.compl A) ∪ (set.compl B)) := sorry
Given these two inclusion proofs, how do I prove set equality, i.e.
def set_deMorgan_eq : A ∩ B = set.compl ((set.compl A) ∪ (set.compl B)) := sorry

Using sets in lean
I'd like to do some work in topology using lean.
As a good start, I wanted to prove a couple of simple lemmas about sets in lean.
For example
def inter_to_union (H : a ∈ set.inter A B) : a ∈ set.union A B := sorry
or
def set_deMorgan : a ∈ set.inter A B → a ∈ set.union (set.compl A) (set.compl B) := sorry
or, perhaps more interestingly
def set_deMorgan2 : set.inter A B = set.union (set.compl A) (set.compl B) := sorry
But I can't find anywhere elimination rules for
set.union
orset.inter
, so I just don't know how to work with them. How do I prove the lemmas?
Also, looking at the definition of sets in lean, I can see bits of syntax, which look very much like paper maths, but I don't understand at the level of dependent type theory, for example:
protected def sep (p : α → Prop) (s : set α) : set α := {a  a ∈ s ∧ p a}
 How can one break down the above example into simpler notions of dependent/inductive types?

LTL model checking with SPIN
I am looking at the SPIN software. I would like to do use it to find models of LTL theories. All the manuals and tutorials talk about verifying properties of algorithms, but I am not interested in that at all. I simply want to find a models of LTL formulas (a corresponding Büchi automaton, I suppose), much like the mace4 or paradox model checkers can find models of FOL formulas. I believe that SPIN should be able to do that, but I am unable to find how in the documentation. Could somebody point to any helpful resources?

How to define an expression translator?
I defined 2 almost identical languages (foo and bar):
theory SimpTr imports Main begin type_synonym vname = "string" type_synonym 'a env = "vname ⇒ 'a option" datatype fooExp = FooBConst bool  FooIConst int  FooLet vname fooExp fooExp  FooVar vname  FooAnd fooExp fooExp datatype barExp = BarBConst bool  BarIConst int  BarLet vname barExp barExp  BarVar vname  BarAnd barExp barExp
A trivial semantics:
datatype fooValue = FooBValue bool  FooIValue int datatype barValue = BarBValue bool  BarIValue int type_synonym fooEnv = "fooValue env" type_synonym barEnv = "barValue env" primrec FooEval :: "fooExp ⇒ fooEnv ⇒ fooValue option" where "FooEval (FooBConst c) e = Some (FooBValue c)"  "FooEval (FooIConst c) e = Some (FooIValue c)"  "FooEval (FooLet var init body) e = (case FooEval init e of Some x ⇒ FooEval body (e(var ↦ x))  _ ⇒ None)"  "FooEval (FooVar var) e = e var"  "FooEval (FooAnd a b) e = (case (FooEval a e, FooEval b e) of (Some (FooBValue x), Some (FooBValue y)) ⇒ Some (FooBValue (x ∧ y))  _ ⇒ None)" primrec BarEval :: "barExp ⇒ barEnv ⇒ barValue option" where "BarEval (BarBConst c) e = Some (BarBValue c)"  "BarEval (BarIConst c) e = Some (BarIValue c)"  "BarEval (BarLet var init body) e = (case BarEval init e of Some x ⇒ BarEval body (e(var ↦ x))  _ ⇒ None)"  "BarEval (BarVar var) e = e var"  "BarEval (BarAnd a b) e = (case (BarEval a e, BarEval b e) of (Some (BarBValue x), Some (BarBValue y)) ⇒ Some (BarBValue (x ∧ y))  _ ⇒ None)"
Typing:
datatype fooType = FooBType  FooIType datatype barType = BarBType  BarIType type_synonym fooTEnv = "fooType env" type_synonym barTEnv = "barType env" inductive fooTyping :: "fooTEnv ⇒ fooExp ⇒ fooType ⇒ bool" ("(1_/ ⊢f/ (_ :/ _))" [50,0,50] 50) where FooBConstTyping: "Γ ⊢f FooBConst c : FooBType"  FooIConstTyping: "Γ ⊢f FooIConst c : FooIType"  FooLetTyping: "⟦Γ ⊢f init : t1; Γ(var ↦ t1) ⊢f body : t⟧ ⟹ Γ ⊢f FooLet var init body : t"  FooVarTyping: "Γ var = Some t ⟹ Γ ⊢f FooVar var : t"  FooAndTyping: "⟦Γ ⊢f a : BType; Γ ⊢f b : BType⟧ ⟹ Γ ⊢f FooAnd a b : BType" inductive barTyping :: "barTEnv ⇒ barExp ⇒ barType ⇒ bool" ("(1_/ ⊢b/ (_ :/ _))" [50,0,50] 50) where BaroBConstTyping: "Γ ⊢b BarBConst c : BarBType"  BarIConstTyping: "Γ ⊢b BarIConst c : BarIType"  BarLetTyping: "⟦Γ ⊢b init : t1; Γ(var ↦ t1) ⊢b body : t⟧ ⟹ Γ ⊢b BarLet var init body : t"  BarVarTyping: "Γ var = Some t ⟹ Γ ⊢b BarVar var : t"  BarAndTyping: "⟦Γ ⊢b a : BType; Γ ⊢b b : BType⟧ ⟹ Γ ⊢b BarAnd a b : BType" inductive_cases FooBConstTypingRev: "Γ ⊢f FooBConst c : t" inductive_cases BarBConstTypingRev: "Γ ⊢b BarBConst c : t" inductive_cases FooLetTypingRev: "Γ ⊢f FooLet var init body : t" inductive_cases BarLetTypingRev: "Γ ⊢b BarLet var init body : t" inductive_cases FooVarTypingRev: "Γ ⊢f FooVar var : t" inductive_cases BarVarTypingRev: "Γ ⊢b BarVar var : t" inductive_cases FooAndTypingRev: "Γ ⊢f FooAnd a b : t" inductive_cases BarAndTypingRev: "Γ ⊢b BarAnd a b : t"
Also I defined a translator from foo to bar:
primrec FooToBar :: "fooExp ⇒ barExp option" where "FooToBar (FooBConst c) = Some (BarBConst c)"  "FooToBar (FooIConst c) = None"  "FooToBar (FooLet var init body) = (case FooToBar init of Some barInit ⇒ (case FooToBar body of Some barBody ⇒ Some (BarLet var barInit barBody)  _ ⇒ None)  _ ⇒ None)"  "FooToBar (FooVar var) = Some (BarVar var)"  "FooToBar (FooAnd a b) = (case (FooToBar a, FooToBar b) of (Some a1, Some b1) ⇒ Some (BarAnd a1 b1)  _ ⇒ None)"
And I'm trying to prove that the translator transforms fooexpressions to barexpressions with similar types:
inductive TypeEquiv :: "fooType ⇒ barType ⇒ bool" (infix "∼" 50) where "FooBType ∼ BarBType"  "FooIType ∼ BarIType" lemma FooToBarFooLetElim: "FooToBar (FooLet x1a fooExp1 fooExp2) = Some barExp ⟹ ∃ barExp1 barExp2. FooToBar fooExp1 = Some barExp1 ∧ FooToBar fooExp2 = Some barExp2" by (metis (no_types, lifting) FooToBar.simps(3) option.case_eq_if option.exhaust_sel) lemma FooToBarPreserveType: "FooToBar fooExp = Some barExp ⟹ Γ1 ⊢f fooExp : t1 ⟹ Γ2 ⊢b barExp : t2 ⟹ t1 ∼ t2" apply (induct fooExp arbitrary: barExp Γ1 Γ2 t1 t2) apply (metis FooBConstTypingRev BarBConstTypingRev FooToBar.simps(1) TypeEquiv.intros(1) option.sel) apply simp apply (metis FooLetTypingRev BarLetTypingRev FooToBar.simps(3) FooToBarFooLetElim option.inject option.simps(5))
And also the transformation preserves semantics of expressions:
inductive ValueEquiv :: "fooValue ⇒ barValue ⇒ bool" (infix "≈" 50) where "v1 = v2 ⟹ FooBValue v1 ≈ BarBValue v2"  "v1 = v2 ⟹ FooIValue v1 ≈ BarIValue v2" lemma FooToBarPreserveValue: "FooToBar fooExp = Some barExp ⟹ FooEval fooExp fooEnv = Some v1 ⟹ BarEval barExp barEnv = Some v2 ⟹ v1 ≈ v2" apply (induct fooExp arbitrary: barExp fooEnv barEnv v1 v2) using ValueEquiv.simps apply fastforce apply simp apply (smt BarEval.simps(3) FooEval.simps(3) FooToBar.simps(3) FooToBarFooLetElim option.case_eq_if option.sel option.simps(5))
I even proved some induction cases. But I can't prove lemmas for
FooToBar (FooVar x)
case.In general It can't be proved that
FooVar x
has a similar type or value toBarVar x
.I guess that
FooToBar
must be more complicated. It must involve also some kind of expression environment or variable mapping. Could you suggest a better signature forFooToBar
? I think such a translator is a trivial thing, but I can't find any textbook describing it. 
SparkAda postcondition for array total
How does one write a Spark postcondition for a function that sums the elements of an array? (Spark 2014, but if someone shows me how to do it for an earlier Spark I should be able to adapt it.)
So if I have:
type Positive_Array is array (Positive range <>) of Positive; function Array_Total(The_Array: Positive_Array) return Positive with Post => Array_Total'Return =  What goes here? is  and so on
I don't need to worry about overflow in my particular case (I know what the total was at initialisation, and it can only monotonically decrease).
Presumably I'll need a loop variant in the implementation, to help the prover, but that should be straightforward variation of the postcondition, so I'm not worried about that yet.

Proving equivalence of programs
The ultimate in optimizing compilers would be one that searched among the space of programs for a program equivalent to the original but faster. This has been done in practice for very small basic blocks: https://en.wikipedia.org/wiki/Superoptimization
It sounds like the hard part is the exponential nature of the search space, but actually it's not; the hard part is, supposing you find what you're looking for, how do you prove that the new, faster program is really equivalent to the original?
Last time I looked into it, some progress had been made on proving certain properties of programs in certain contexts, particularly at a very small scale when you are talking about scalar variables or small fixed bit vectors, but not really on proving equivalence of programs at a larger scale when you are talking about complex data structures.
Has anyone figured out a way to do this yet, even 'modulo solving this NPhard search problem that we don't know how to solve yet'?