forked from nasa/pvslib
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathCHANGES.txt
342 lines (274 loc) · 13.2 KB
/
CHANGES.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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
NASA PVS Library 6.0.10 (xx/xx/xx)
6.0.10 (xx/xx/xx)
- Added fast_approx
- Added TCAS II TA and RA core logics, Well-Clear definitions, and
DAIDALUS algorithms
- Added affine arithmetic contribution (thanks to Mariano Moscato)
- Improved approximations in reals@srt_approx, lnexp_fnd@ln_approx,trig_fnd@atan_approx
- Added best_rational to reals, which is used in interval_arith
- interval_arith:
. Added rational_interval
. Improved efficiency in strategies based on interval arithmetic
. Parameter N has been dropped. Accuracy and precision are both governed by parameter PRECISION.
- CCG:
. Removed typed measures in measures.pvs (it is Sign3) in theory measures.pvs
. Renamed symbol "+" for Sign3 as "Plus3" in theory measures.pvs
. Renamed type "measure_matrix" as "Measure_Matrix" in theory measures.pvs
. Added criterion for positivity based on size of circuits in theory matrix_wdg.pvs
6.0.9 (November 10 2014)
- General library updates
- Added PVSioChecker
- Added Stum and Tarski's development
- Added Bernstein (unfortunately, strategy is not working yet due to some changes in PVS 6.0)
6.0.8 (March 14 2014)
- Updated digraph (thanks to Andreia Avelar Borges)
- Updated ACCoRD, lnexp_fnd, analysis, lebesgue, trig_fnd, and complex_integration
6.0.7 (February 28 2014)
- Corrected misspelling of "schwarz" in vectors, vect_analysis, and ACCoRD
- vectors:
Added vectors_4D.
Renamed "sq" in vectors as "sos" (sum of squares). This change avoids a name clash with reals@sq
The following lemmas changed names: sqv_sq -> sqv_sos, norms_eq_sq -> norms_eq_sos.
- interval_arith:
Removed options const and rats from numerical and interval. These options are not needed anymore.
- Moved Stosic's contributions choice_facts and refaniment_relations to set_aux
- Moved Stosic's contribution allen to interval_arith
- Added analysis_ax, an axiomatic version of analysis
- Added development Sturm, which includes the decision procedure sturm for univariate polynomials
- pvsio and proveit:
Added options -disable-oracles, -disable <oracle>, -enable <oracle>, to disable all oracles, disable
<oracle>, or reenable <oracle>, respectively. Currently, the only
oracle that is supported is MetiTarski.
Fixed options -tex and -txt in script proveit. These options generate latex and text proofs from PVS proof scripts.
6.0.6 (September 4 2013)
- Added PVS 6.0 patches (thanks to Sam Owre)
- Fixed small bugs in metit and added support for some symbols, e.g., =>, &, <=> (thanks to
Viorel Preoteasaa)
- Added confluence of orthogonal TRS (thanks to Ana Rocha and Mauricio Ayala)
6.0.5 (June 13 2013)
- Fixed the broken proof in 6.0.4b
- Improved interval_arith to include support for safe and proper arithmetic
operations.
- Improved strategies in interval_arith, e.g., added support to let-in expressions
- Fixed old bugs in PVSio, e.g., added support for constant semantic attachments
- Integrated MetiTarski 2.2/Z3 4.3.1 to PVS through the proof rule metit (William
Denman's contribution). The proof rule metit solves universally quantified first-order
formulas over real-valued expressions involving trignometric functions, ln, exp, and sqrt.
6.0.4b (May 13 2013)
- Special distribution for VSTTE Summer School 2013 (1 proof is broken).
- Added refinament relations (Dragan Stoic's contribution)
- Improved interval_arith to include support for conditional expressions
- Added PVS patches
6.0.4 (March 13 2013)
- Removed orphan and outdated theories
- Added PVS patches
6.0.3 (Feb 23 2013)
- Added Allen interval temporal logic (Dragan Stoic's contribution)
6.0.2 (February 13 2013)
- Added satisfiability and validity checker for simplify quantified formulas and
Boolean expressions via interval arithmetic (see strategy interval in interval-arith)
- Added sets as list to structures
6.0.1 (February 3 2013)
- Added exponential to interval_arith
6.0 (January 26 2013)
- Updated to PVS 6.0. This version of the library includes several upgrades, e.g.,
structures:
- Added for-loops and iterations (for_iterate, for_examples).
- Added Maybe and Unit types (Maybe, Unit).
- Added a preliminary array theory tailored towards ground evaluation (arrays).
- Added a generic branch and bound algorithm (branch_and_bound).
- Added a type of lists of n elements (listn).
- Added array to list functions (array2list).
interval_arith:
- Added a formal proofs of Inclusion and Fundamental theorems of interval arithmetic.
- Completely redefined strategies: numerical and interval.These strategies
are now based on computational reflection and are much more efficient than
the previous strategies numerical and instint.
- For a complete list of strategies available in interval_arith, use
the proof command interval-about.
digraphs:
- Revisited several definitions and lemmas.
- The packages Extrategies and Field, which are now part of PVS, have been
completely revisited. The strategies in these packages handle TCCs in a
much better way. Unfortunately, this may cause some strategies to behave in a
slightly way and to break some old proofs. In particular, SKOLETIN
may generate proofs in a different order. In most cases, the old
behavior of SKOLETIN can be simulated by setting the option :old? to t.
Extrategies provides new strategy combinators for building strategies.
In particular, it includes the proof command deftactic for defining local
strategies (called tactics), whose scope is the branch of the proof where the
tactic is declared. For a complete list of strategies available in
Extrategies and Field, use the proof command extrategies-about and
field-about.
- The Bernstein development is still missing in this version of the library.
It will be released soon.
5.8 (December 21 2011)
- Several library updates (linear_algebra, ACCoRD, orders, etc)
5.7.6 (August 22 2011)
- Simplified induction schema for for-loops in structures@for_iterate.
5.7.5 (August 5 2011)
- Added lemmas in real/minmax and vectors/ECEF.pvs
5.7.4 (July 15 2011)
- Added library Bernstein (inluding the tool Grizzly)
- Added lemmas to series/series.pvs
5.7.3 (June 9 2011)
Term Rewrite System library updated to PVS 5.0. Thanks to Andre Galdino,
Andreia Borges and Mauricio Ayala, University of Brasilia, Brazil
5.7.2 (May 27 2011)
Uncommented and fixed proofs in orders and while
5.7.1 (May 20 2011)
Updated to handle last minute PVS 5.0 changes
5.7.0 (May 10 2011) Upgraded to PVS 5.0
Interval library renamed interval_arith
5.6.0 Linear Algebra library added
5.5.0 not_one_element? and connected? predicate added in analysis libraries
5.4.9 lebesgue added. Thanks to David Lester!
5.4.8 measure_integration updated. Thanks to David Lester!
5.4.7 Term-Rewriting-System (TRS) added. Thanks Andre Luiz Galdino and Mauricio Ayala Rincon!
5.4.6 vect_analysis/vect2_cont_comp AND vect_analysis/vect2_cont_comp2
5.4.5 continuous decoupled from convergence to some extent
5.4.3 Antony's convex functions and more on vector metric speaces
5.4.2 Lester's metric_space library added
5.4.1 more compactness results in analysis and vect_analysis libraries
5.4.0 vect_analysis library: derivatives of vector-valued functions
5.3.9 analysis library: metric_spaces, continuity, and compactness added
5.3.8 power library updated, sqrt(2) irrational in numbers library
5.3.7 some lemmas added to vectors library
5.3.6 vect_analysis library created
5.3.5 continuity of vector functions in vectors library
5.3.4 connected-set added to analysis
5.3.3 made name changes in reals and analysis ("opposite" -> "negative")
5.3.2 made name changes in vectors library to gain consistency (see NAME-CHANGES.txt)
5.3.1 quadratic_minmax replaced by quad_minmax in reals library
5.3 definition of Nz_vector changed in vectors library, more parallel stuff
5.2.9 name changes in vectors library
5.2.8 mods to quadratic and sqrt theories in reals library
5.2.7 more small changes to vectors library
5.2.6 small changes to vectors library, sq(v) def changed, theory det2D added
5.2.5 a few lemmas added to analysis
5.2.4 a few lemmas added to reals and vectors
5.2.3 a few lemmas added to trig and vectors, vect2D_trunc theory added
5.2.2 added theories angles_2D, between_2D to vectors library -- March 14, 2008
5.2.1 A few proofs were fixed -- March 6, 2008
5.2 Changes (Feb 29, 2008)
--------------------------
-- Add library "fs" which is just a holding place for theories that
should be in finite_sets. These will hopefully be moved there
in the next release of PVS.
-- moved abs_props and real_facts into reals library. NOTE
(stop-rewrite "abs_0") (stop-rewrite "abs_nat") may
be helpful in repairing broken proofs that use analysis library
or reals@abs_lems. Can also use AUTO_REWRITE- in theory.
5.1.5 --> added vectors_sign theories to vectors library
5.1.4 --> added cross_3D to vectors library, sigma over vector-valued
functions 2-11-08
5.1 Changes (Jan 25, 2008)
--------------------------
-- The product operator added to the reals and ints library. A generic
theory is provided in product.pvs, which is similar to sigma.pvs.
The following theories provide additional theorems for specific domains:
product_below, product_int, product_nat, product_posnat, product_upto
-- An experimental alternate finite sequences library "fseqs" added to
structures library
5.0 Changes (Jan 11, 2008)
--------------------------
-- The types of the inverse trig functions have been simplified -- no
internal function calls
4.9 Changes (Jan 2, 2008)
---------------------------
-- Number Theory library contents moved to ints
-- ints library made more consistent with prelude
4.8 Changes (Dec 17, 2007)
---------------------------
-- New Scott Library provided by David Lester of Manchester University
-- New sigma_set library provided by David Lester of Manchester University
-- New lemmas in series library about absolute convergence
-- Improvements to algebra library -- factor groups added
4.7 Changes (Nov 20, 2007)
---------------------------
-- improvements to atan_approx and trig_approx in trig_fnd library
-- improvements to interval library (Interval-4.a)
-- improvements to manip
4.6 Changes (Nov 8, 2007)
---------------------------
-- Improved sigma definition (simpler) -- old_sigma* theories retained
NOTE: this will break some proofs, but an extra (expand "sigma") or
replacing (expand"sigma") with (rewrite "sigma_rew") often easily
fixes the proofs
4.5 Changes (Nov 1, 2007)
---------------------------
-- Add quad_minmax to reals library
-- improved closest_approach* in vectors library
4.4 Changes (Sept 17, 2007)
---------------------------
-- New topology library added
-- Some new lemmas in trig_fnd
-- A few additions to algebra libray
4.3 Changes (July 19, 2007)
---------------------------
-- graphs library: Menger's Theorem now general due to Jon Sjogren
4.2 Changes (May 10, 2007)
---------------------------
-- complex library updated by David Lester
-- added co_structures library with Jerry James's sequence theories
-- fixed unproved theorems in float (Munoz)
-- proof in lnexp_fnd/hyperbolic repaired (Lester)
4.1 Changes (April 24, 2007)
---------------------------
all proofs in complex library repaired by David Lester
4.0 Changes (Dec 8, 2006)
-------------------------
updated to PVS 4.0
3.2.2 Changes (Mar 24, 2006)
-------------------------------
moved nth_derivatives, and taylors from series to analysis library.
simplified definition of 'powerseq" in series library.
3.2.1.9 Changes (Nov 30, 2005)
-------------------------------
restored float library
3.2.1.8 Changes (Oct 25, 2005)
-------------------------------
Removed IMPORTING reals@ in reals library that was causing
some problems.
3.2.1.7 Changes (Sept 15, 2005)
-------------------------------
Added new intervals library
3.2.1.6 Changes (July 19, 2005)
-------------------------------
A matroids and mappings theory was added to the graphs library.
3.2.1.5 Changes (May 12, 2005)
------------------------------
NAME-CHANGES:
composition_continuous1 -> composition_cont
composition_continuous2 -> composition_cont_set
composition_continuous3 -> composition_cont_fun
formatting in analysis
update to sets_aux, orders
3.2.1.4 Changes (April 21, 2005)
--------------------------------
Split sets_aux into sets_aux and an orders library
fixed atan2_props
3.2.1.3 Changes
---------------
The directory lnexp now contains an axiomatic version.
The foundational version is in lnexp_fnd.
trig -- updated to match foundational version (trig_fnd).
3.2.1.2 Changes
---------------
float -- new library
reals -- factorial props
lnexp -- ln_exp_series_alt modified
3.2.1.1 Changes
-------------
trig_fnd -- improvements to exp_approx, ln_approx, tan_approx,
trig_ineq, and trig_degree
lnexp -- theories ln_exp_series_alt, ln_exp_ineq added
3.2.1 Changes
-------------
reals -- new theory: log_nat
reals -- sqrt_approx updated
lnexp -- ln_approx updated
lnexp -- infinite series for ln added in theory ln_series
series -- integral_powerseries theorem completed
analysis -- integral_chg_var, integral_dif_doms added,
fundamental4 lemma added.