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

How to merge multiple data frames based on two columns?
I'm quite new to R and need some help.
I have multiple data frames for data collected over 4 days. Each of the data frames looks like this (put very simply):
Lat Long PM 33.9174 151.2263 8 33.9175 151.2264 10 33.9176 151.2265 9 33.9177 151.2266 8
I want to merge multiple data frames based on their matching Long and Lat values, to average out all 'PM' values at a particular location. The end result will look something like this (for the 13th  16th Feb):
Lat Long PM.13th Feb PM.14th Feb PM.15th Feb **Mean** 33.9174 151.2263 8 9 11 9.33 33.9175 151.2264 10 11 12 11 33.9176 151.2265 9 14 13 12 33.9177 151.2266 8 10 11 9.66
I understand that merging 2 data frames is easy enough:
df = merge(data1, data2, by.x = c("Lat", "Long"), by.y = c("Lat", "Long"))
But how do I merge multiple dataframes based on matching Longitude and Latitude values?
Also, is there a way I can filter the data so that it will match up data which is within 0.001 Lat/Long value of each other? (Currently I am rounding the Lat/Long data to 3 decimal places, but it is duplicating my data).
Thank you!

R: How to expand a tidy table of ranked words
I have a tidy data frame of the form
> data.frame("topic" = c(1,1,2,2,3,3), "term" = c("will", "eat", "go", "fun", "good", "bad"), "score" = c(0.3, 0.2, 0.5, 0.4, 0.1, 0.05)) topic term score 1 1 will 0.30 2 1 eat 0.20 3 2 go 0.50 4 2 fun 0.40 5 3 good 0.10 6 3 bad 0.05
So the purpose of the table is to store the top n (in this case 2) scoring terms for each topic. This table is easy to work with, but I want to be able to view the data like this:
topic1 topic2 topic3 1 will go good 2 eat fun bad
In this new table, I don't care about the scores, I just want to see the top n scoring terms for each topic. I feel like this should be doable using
dplyr
or something but I'm not great with R. 
R Add table of variable row numbers in the middle of an existing Excel sheet with openxlsx
I load an existing Excel sheet (template) with openxlsx.
I add a table starting at a specific column/row combination. Say cell A1.
The template contains more text that has to remain under the table. But I don't know yet how long the table will be. The text is now in cell C1 and if the table takes more than 3 rows than the text is overwritten with the table. I want the table to be written on newly inserted lines.
One possible solution I look for is how to insert a single row. At the moment just before writing the table to Excel I know the number of rows. So if there would be a function to insert a single row I could at precisely enough single rows programmatically.
These lines of code now overwrite what is there:
library(openxlsx) wb < loadWorkbook("my_template.xlsx") data < mtcars[1:sample(1:10, 1), ] # I NEED CODE TO INSERT A ROW FOR EVERY ROW IN THE DATA # BECAUSE THE TABLE STARTS AT CELL A1 AND CONTENTS OF CELL C1 SHOULD REMAIN UNDER THE TABLE # Insert table of variable height (rows) writeData(wb = wb, sheet = 1, x = data) saveWorkbook(wb, "file.xlsx", overwrite = T)
Thanks, Jiddu

Finding all Z3 satisfying models using C language not C++?
I want to find all satisfying models using Z3 in C language (I'm not looking for C++ code).

Proving the 100 Prisoners and a lightbulb with Dafny
Consider the standard strategy to solve the 100 prisoners and a lightbulb problem. Here's my attempt to model it in Dafny:
method strategy<T>(P: set<T>, Special: T) returns (count: int) requires P > 1 && Special in P ensures count == (P  1) decreases * { count := 0; var I := {}; var S := {}; var switch := false; while (count < (P1)) invariant count <= (P1) invariant count > 0 ==> Special in I invariant Special !in S && S < P && S <= I && I <= P decreases * { var c : c in P; I := I + {c}; if c == Special { if switch == true { switch := false; count := count + 1; } } else { if c !in S && switch == false { S := S + {c}; switch := true; } } } assert(I == P); }
It fails, however, to prove that in the end
I == P
. Why? I probably need to strengthen the loop invariant even further, but can't imagine where to start from... 
Any Java open source projects using verification?
Does anyone know of any Java open source libraries/projects that either:
 Use formal specifications to define their API contract (e.g. with JML, or a similar contract language specifying pre, post conditions).
 Use contract specifications within the code in general (e.g. through annotations provided by something like OpenJML (http://www.openjml.org/) or OVal (http://oval.sourceforge.net/)).

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'?

Is there a way to find out what is causing 'No Instance Found' on run in Alloy?
I have written in model using Alloy. However for certain conditions running the predicate to find an instance is failing and it says that no instance can be found. I tried increasing the bound to about 16 instances, yet it does not find any instance.
Is there any way I can debug this so that I can see which facts are failing which is causing Alloy not being able to find an instance?
Thanks !