| products/sources/formale sprachen/PVS/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: CHANGES.txt Sprache: TextOriginal von: PVS© |
|
||||||
|
NASA PVS Library 6.0.9 (11/10/14)
6.0.10 (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 anymo - 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 polyno - pvsio and proveit: Added options -disable-oracles, -disable <oracle>, -enable <oracle>, to disable all oracles, di <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 fro 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 Rinco 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. ¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
