[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] Survey on NASA PVS Library use



Dear PVS user:
      We would like to make several improvements in the naming
schemes being used in the NASA libraries, and would like to
get some idea of the potential impact of library changes on
the user community.  We would also like to gain some feedback
on the value of our libraries to you to help us prioritize our
future efforts.  Therefore we would appreciate your help by
answering this short survey.  Send reply to:

   R.W.Butler@larc.nasa.gov

Thanks,

Rick Butler
---------------------------

   1. Which of the following PVS Libraries have you used?

           ____ algebra
           ____ analysis
           ____ calculus
           ____ complex
           ____ digraphs
           ____ fixedpoints
           ____ graphs
           ____ ints        (or nat_funs, div, mod)
           ____ lnexp
           ____ number_theory
           ____ reals
           ____ series
           ____ sets_aux    (or powersets)
           ____ structures  (or arrays, bags)
           ____ trig
           ____ trig_fnd
           ____ vectors
           ____ other ______________________________________
                      ______________________________________
                      ______________________________________



   2. Which of the following strategy packages have you used:

           ____ Manip (NASA Langley; included with NASA libraries)
           ____ Field (NIA; included with NASA libraries)
           ____ PVSio (NIA; included with NASA libraries)
           ____ ProofLite (NIA)
           ____ TAME (NRL)
           ____ Other, publicly distibuted strategies: __________
           ____ Other, undistributed strategies: ___________
           ____ Personally developed strategies: ___________
           ____ Invoked any of the packages above programmatically
                 (e.g., to implement higher-level strategies)



   3. Which of the following Manip/Field capabilities have you used:

           ____ MULT-BY, DIV-BY, CROSS-MULT
           ____ FACTOR
           ____ "Emacs interface or proof maintenance (e.g., TAB-y)"
           ____ SWAP, GROUP, EQUATE
           ____ TRANSFORM-BOTH
           ____ MULT-EQ, MULT-INEQ, MULT-CASES
           ____ extended expressions (e.g. (! + (->* "cos") 1))
           ____ strategy writing support functions
           ____ FIELD
           ____ GRIND-REALS, REAL-PROPS
           ____ SKEEP
           ____ CANCEL-FORMULA
           ____ SKOLETIN
           ____ ADD-FORMULAS, NEG-FORMULA
           ____ CANCEL-BY, CANCEL-FORMULA
           ____ REPLACES
           ____ Other Manip strategies: ______________________________________
           ____ Other Field strategies: ______________________________________


   4. What additional libraries or strategies would be useful to you?

           ________________________
           ________________________
           ________________________
           ________________________
           ________________________

   5. What do you like about the NASA libraries?
          ____________________________________________________________________
          ____________________________________________________________________
          ____________________________________________________________________
          ____________________________________________________________________
          ____________________________________________________________________
          ____________________________________________________________________
          ____________________________________________________________________

   6. What do you dislike about the NASA libraries?
          ____________________________________________________________________
          ____________________________________________________________________
          ____________________________________________________________________
          ____________________________________________________________________
          ____________________________________________________________________
          ____________________________________________________________________
          ____________________________________________________________________