PAL CARD CATALOG ENTRY

SHORT DESCRIPTION

Reference manual for Penelope, an interactive environment for verification


MOVEMENT WITHIN THE PAL CARD CATALOG
Move to top-level taxonomy
Move to keyword list

ASSET PROFILE

UNIT NAME
PENRM
VERSION
STARS-AC-A023/004/00, 26-FEB-94
ORIGIN
ASSET
REVIEW CODE
OK
INET ADDRESS
librarian@source.asset.com
AUTHOR
Carla Marceau
UNISYS
RIGHTS
Approved for public release; distribution unlimited
COPYRIGHT
1994 UNISYS
LOCATION
ASSET
PAL

FILE LISTING

Directory Display


languages/ada/docs/penelope/penrm:
  File Name                 Size
  ---------                 ----
  README                   1,642
  penrm.zip              258,380
  DIRUPD.D1                  174
  DIRUPD.SUB*                258
  T*                          31
  a1bintre.sid             5,416
  a1btrees.sid             5,196
  a1cli.sid                5,953
  a1dag.sid                6,229
  a1darray.sid             5,818
  a1errmsg.sid             4,566
  a1fl_mgr.sid             5,165
  a1gram.sid               4,352
  a1hostdp.sid             4,329
  a1hshfcn.sid             4,538
  a1hshmap.sid             5,763
  a1lex.sid                5,405
  a1lists.sid              5,542
  a1ordset.sid             5,308
  a1parse.sid              5,115
  a1pgfile.sid             6,472
  a1scan.sid               6,873
  a1set.sid                5,569
  a1slists.sid             4,606
  a1sort.sid               4,287
  a1stack.sid              5,048
  a1state.sid              4,759
  a1string.sid             6,976
  a1vmslib.sid             4,520
  a2bintre.sid             5,515
  a2btrees.sid             4,964
  a2cisc.sid               4,635
  a2cssc.sid               4,382
  a2docref.sid             4,921
  a2errmsg.sid             4,597
  a2ilists.sid             4,579
  a2lists.sid              5,534
  a2ltrees.sid             6,009
  a2ordset.sid             5,139
  a2pgfile.sid             4,958
  a2scaner.sid             5,116
  a2sintf.sid              7,801
  a2slists.sid             4,635
  a2stack.sid              4,785
  a2string.sid             5,150
  a2sutils.sid             7,628
  a2termio.sid             5,250
  a970.sid                 4,500
  a9x_tutr.sid             6,492
  a_aah.mid                9,469
  a_abwg.mid               8,338
  a_aces.mid               7,892
  a_acvc.mid               7,218
  a_ada.mid                3,062
  a_ada9x.mid              7,395
  a_adacmt.mid             3,019
  a_adastyle.mid           5,582
  a_adaui.mid              2,967
  a_artewg.mid             6,631
  a_asiswg.mid            13,481
  a_atip.mid               7,376
  a_compat.mid             3,226
  a_compiler.mid           3,972
  a_crease.mid             3,681
  a_devtool.mid           10,742
  a_dualuse.mid            4,191
  a_edtrain.mid            4,177
  a_events.mid             2,682
  a_evinfo.mid             2,617
  a_grammar95.mid
                           3,120
  a_graphics.mid           2,966
  a_irds.mid               3,047
  a_mil498.mid             3,282
  a_news.mid               3,002
  a_nsaicw.mid             6,889
  a_pcis.mid              12,019
  a_piwg.mid               4,077
  a_policy.mid             3,787
  a_report.mid             2,678
  a_resource.mid           3,264
  a_rm83.mid               3,164
  a_rm95.mid               3,414
  a_rrg.mid                6,900
  a_trans.mid              2,761
  a_usage.mid              4,908
  abstract.sid             5,850
  ace.sid                  7,372
  acomps.sid              23,979
  acq_hb.tid               4,084
  act.sid                  5,087
  activity.mid             6,568
  ada                         22
  ada95_oo.tid             2,965
  ada9xbhlp.tid            3,304
  ada9xbinf.tid            3,257
  ada_fft.sid              4,464
  ada_met1.sid             5,800
  ada_sda.sid              6,626
  ada_tutr.sid             6,366
  adacli.sid               4,496
  adaed.sid               12,678
  adafair8.sid             4,291
  adaform.sid              3,600
  adamode.sid              3,228
  adapp.sid                5,664
  adar.sid                 5,927
  adaref.sid               3,151
  adasage.mid             16,083
  adastyle.tid             4,387
  adobefm.sid              5,746
  afilemgr.sid             4,859
  afscoo.tid               3,094
  afsll.tid                2,781
  ahostdep.sid             4,236
  ahostlib.sid             5,956
  ajpo.mid                11,292
  aloaf.tid                3,709
  alsp.sid                 4,779
  alt_srcs.tid             3,464
  anetcat.tid              2,448
  aops.tid                 2,902
  apath.sid                5,273
  apfat.sid                4,753
  applblue.tid             3,092
  arc.tid                  2,525
  arpc.sid                 5,823
  arps.sid                 5,199
  arts.sid                 4,319
  asap.sid                 5,700
  asc.sid                  5,328
  asento.sid               5,729
  asg.tid                  3,196
  asr.mid                 11,814
  asruh.tid                2,928
  assetcat.tid             2,825
  assetfaq.tid             2,362
  assetool.sid             4,674
  astyle.sid               5,256
  asynntry.sid             3,501
  ausrinfo.tid             2,944
  avlada9x.sid             6,771
  ayacc.sid                7,312
  bd3.sid                  5,098
  benchmrk.sid             5,323
  bgi.tid                  3,111
  bgt.sid                  5,899
  bit.sid                  4,212
  bplustre.sid             5,412
  brada.sid                3,281
  bstyle.sid               4,967
  c01crs.sid              13,046
  c01crsa.sid             12,718
  c01crsb.sid             12,729
  c02crs.sid               4,253
  c03crs.sid               4,930
  c05.tid                  2,717
  cais.sid                 6,566
  calc.sid                 4,634
  calc1.sid                5,075
  calc2.sid                5,013
  canada.sid               5,996
  cas.sid                  4,917
  cas2.sid                 4,881
  cas3.sid                 4,941
  cat.sid                  5,967
  cat2.sid                 5,966
  cbind.sid                3,544
  cbreak.sid               4,355
  cdshows.tid              3,559
  cdupdate.sid             4,538
  cepa.tid                 3,329
  cepg.tid                 3,215
  cert1.sid                7,319
  cfrp2.tid                3,923
  cfrp3.tid                5,681
  ch2ada.sid              10,482
  chiron.sid               8,761
  class.sid                6,241
  cli.sid                  4,483
  cli2.sid                 5,693
  clp.sid                  5,073
  cma.sid                  4,341
  cmm.tid                 11,627
  codguide.tid             2,709
  codywait.sid             5,998
  comphdbk.tid             3,736
  compmeas.sid             5,842
  compord.sid              5,332
  composer.sid             5,215
  concept.tid              4,280
  constrct.sid             5,723
  contract.tid             3,741
  countada.sid             4,889
  cpa.sid                  3,708
  cpuclock.sid             4,334
  cpyright.tid             7,420
  createtb.sid             6,050
  cset.sid                 4,970
  csparts.sid              8,204
  cspcs.tid                3,436
  cstrings.sid             5,561
  curses.sid               4,302
  custio.sid               5,116
  d_armydata.sid           8,543
  d_charutil.sid           8,713
  d_dateform.sid          11,258
  d_dsrscat.tid            5,707
  d_ebcdic.sid             9,099
  d_immedio.sid            9,386
  d_keyfile.sid            8,935
  d_personel.sid           9,811
  d_report.sid            13,807
  d_scrnmgr.sid           14,359
  d_seqfile.sid           10,206
  d_strutil.sid            9,774
  d_strutil2.sid          11,504
  d_termio.sid            14,635
  d_userin.sid             9,831
  d_vmsutil.sid            8,337
  d_windowio.sid          10,378
  dadaism.sid              4,884
  dames.sid                5,906
  dapm.tid                 2,841
  date.sid                 4,798
  dcdsdata.tid             3,711
  dcdsfram.tid             3,255
  dcdslcm.tid              3,689
  dd.sid                   5,634
  delguide.tid             3,101
  dfreuse.tid              3,905
  diana.sid                5,824
  did2167a.sid             6,634
  dine.sid                 3,981
  diplot.sid               5,628
  dir.tid                  5,578
  dl_hb.tid                5,804
  dlist.sid                4,416
  docmgr.sid               5,803
  dstr1.sid                4,031
  dstr2.sid                4,144
  dstr3.sid                4,581
  dunit.sid                4,246
  ed2.sid                  5,271
  editada.sid              4,864
  editor.sid               4,780
  eduasr.tid               2,312
  edufor.tid               2,543
  eduobj.tid               2,274
  eduperrs.tid             2,314
  edupnote.tid             3,171
  eduprod.tid              2,228
  edutech.tid              2,886
  eduterm.tid              2,165
  edututor.tid             2,163
  email.mid                5,540
  engrhdbk.tid             3,657
  env.sid                  4,281
  esm.sid                  5,319
  eti.sid                  4,849
  evalra.tid               3,428
  except.tid               2,200
  expert.sid               4,460
  far.tid                  2,994
  fcheck.sid               5,424
  feldman.tid              4,116
  fget.sid                 4,370
  filecomp.sid             5,231
  flister.sid              4,429
  fof.sid                  4,732
  form2.sid                5,400
  formater.sid             5,000
  franplan.tid             3,867
  ftp.sid                  5,391
  gad.sid                  5,602
  garbage.sid              4,261
  gks.sid                  4,102
  gmhf.sid                 4,719
  gnat.mid                12,061
  gnatnews.tid             2,543
  gnuada.sid               5,249
  gpriqueu.sid             6,247
  grace.tid                2,182
  gram2.sid                4,865
  grammar.sid              4,666
  grpthndl.sid             6,730
  gset.sid                 4,181
  halstead.sid             4,557
  hartston.sid             5,857
  help.sid                 5,417
  hia.tid                  5,115
  image.sid                7,493
  inel.mid                 4,311
  inetbks.tid              2,307
  inetnote.tid             2,857
  intro9x.tid              3,888
  intro9xh.tid             3,693
  iofile.sid               4,119
  iom.tid                  3,828
  iospt.sid                5,236
  irsdiana.tid             3,563
  ismatch.sid              3,975
  jpmobnch.sid             4,494
  kalman.sid               4,617
  languages                   18
  lart.sid                 4,718
  libcap.tid               3,641
  libcaps.tid              2,985
  libdev.tid               3,954
  libops.tid               6,174
  library.tid              3,026
  limprior.sid             4,467
  list.sid                 4,426
  listpack.sid             3,689
  logical.sid              4,025
  lovelace.tid            11,792
  lparse.sid               3,983
  m36.sid                  5,378
  machunix.tid             3,130
  manpower.sid             5,095
  math2.sid                4,632
  mathfun.sid              4,603
  matrix.sid               4,332
  mccabe.sid               4,909
  mccormic.tid             4,054
  mesageio.sid             4,212
  mims.sid                 4,880
  mindex.tid               4,633
  mlib.sid                 4,241
  mlib2.sid                4,646
  mman.sid                 4,233
  mmgr.sid                 4,900
  model.tid                3,961
  mosaic.tid               2,516
  motif.sid                4,545
  motif2.sid               6,219
  namelist.sid             4,010
  napp.sid                 6,739
  nato_ru.tid              3,536
  nccpm.tid                3,174
  netio.sid                6,191
  netmio.sid               6,245
  newabs.sid               5,666
  newsasr.tid              4,099
  newssnap.tid             2,823
  nrg.sid                  4,966
  nsrd.tid                 3,492
  nwg1.sid                 5,636
  nwg2.sid                 5,885
  nyu.mid                  6,652
  occ.sid                  4,569
  ode.sid                  4,241
  page.sid                 4,817
  pager2.sid               5,490
  palccat.sid              6,654
  palp.tid                 4,095
  palshow.tid              4,080
  panal.sid                4,717
  paradise.sid             4,980
  parser.sid               4,964
  pattern.sid              5,156
  pcte.sid                 4,434
  pctebrsr.sid             6,847
  pendemo.tid              5,270
  penfound.tid             4,935
  penrm.tid                5,473
  penverfy.tid             5,460
  perform.sid              5,107
  permutat.sid             4,584
  pip.tid                  2,943
  plot.sid                 5,446
  pmmedesc.tid             3,026
  pmmell.tid               2,926
  poa.sid                  4,697
  posix.sid                4,104
  posix2.sid               3,993
  pot.sid                  4,818
  pplanner.sid             5,056
  pret.sid                 5,510
  prior.sid                4,533
  prismdd.tid              2,976
  prismlm.tid              3,393
  prismug.tid              3,037
  procdef.tid              8,851
  proceng.tid              4,987
  procimp.tid              3,898
  prof.sid                 5,638
  prologue.sid             4,694
  prp.sid                  4,753
  pter.tid                 3,462
  ptf.sid                  7,882
  q.sid                    6,073
  qsap.sid                 5,036
  qsort.sid                3,694
  ran2.sid                 4,377
  ran3.sid                 5,958
  ran4.sid                 4,064
  random.sid               4,211
  rapport.sid              5,123
  rddb.tid                 3,769
  reguide.tid              6,999
  renews.tid               4,747
  repos1.tid               3,023
  repos2.tid               2,662
  reserve.sid              4,671
  ressm.sid                4,540
  reuseag.tid              8,737
  reuseed.tid              3,699
  reuseed2.tid             3,827
  reuseprc.tid             7,320
  rgb.sid                  5,728
  rig.tid                  3,910
  rig_bidm.tid             3,617
  rig_glos.tid             3,064
  rlf.sid                  7,185
  rm83_rdr.sid             5,195
  rm9x_rdr.sid             5,133
  rm9xhtml.tid            23,748
  rpc.sid                  4,680
  rsm.tid                  4,290
  rsr.sid                  4,682
  rt.sid                   5,666
  rudstone.sid             5,438
  ruguide.tid              3,274
  safeio.sid               4,702
  same1.sid                4,802
  same2.sid                4,514
  sd.sid                   5,563
  sdepdec.sid              4,704
  sdepdg.sid               5,277
  search.sid               4,470
  seeanal.tid              3,114
  seecomp.tid              3,234
  seedemo.tid              3,035
  seell.tid                3,318
  seemeth.tid              3,544
  seetest.tid              2,813
  seetr.tid                2,835
  sei.mid                  4,862
  sei_cm02.tid             3,669
  sei_cm03.tid             3,718
  sei_cm04.tid             3,701
  sei_cm05.tid             3,670
  sei_cm06.tid             3,655
  sei_cm07.tid             3,690
  sei_cm08.tid             3,694
  sei_cm09.tid             3,675
  sei_cm10.tid             3,791
  sei_cm11.tid             3,683
  sei_cm12.tid             3,663
  sei_cm13.tid             3,773
  sei_cm14.tid             3,800
  sei_cm16.tid             3,732
  sei_cm19.tid             3,678
  sei_cm20.tid             3,748
  sei_cm21.tid             3,747
  sei_cm22.tid             3,788
  sei_cm24.tid             3,701
  sei_cm25.tid             4,268
  sei_cm26.tid             3,681
  sei_cm27.tid             3,899
  sei_em01.tid             4,308
  sei_em02.tid             3,924
  sei_em03.tid             4,081
  sei_em05.tid             3,752
  sei_em08.tid             3,969
  sei_em09.tid             4,218
  sei_rpts.tid             4,431
  sei_se.tid               3,737
  seidocs.mid             15,520
  sflcdr.tid               3,623
  sflcfd.tid               3,085
  sftp.sid                 5,024
  sgmldtd.tid              2,718
  sgmlll.tid               2,678
  sgmlpr.tid               2,709
  sgmlug.tid               3,212
  sinst.sid                4,684
  slist.sid                3,917
  smallada.sid             9,145
  smetric.sid              4,965
  smg.tid                  8,518
  smtp.sid                 5,356
  sortarry.sid             4,250
  specpars.sid             4,917
  spell2.sid               5,467
  sptter.tid               3,888
  sql1.sid                 4,495
  sql2.sid                 5,642
  sqltg.sid                4,798
  sritests.sid             3,770
  srl.sid                  5,098
  stab1.sid                5,074
  stab2.sid                5,370
  stack.sid                4,272
  stnd.sid                 5,581
  strcomp.sid              4,719
  stringer.sid             3,895
  stub2.sid                4,793
  stubber.sid              4,526
  supcomp.tid              3,323
  sw_reuse.tid             5,438
  swcompsp.tid             3,061
  sysmeas.tid              8,370
  ta_83intro.tid           3,039
  ta_83over.tid            3,042
  ta_95child.tid           2,940
  ta_95concur.tid
                           2,970
  ta_95distrb.tid
                           2,961
  ta_95intro.tid           3,040
  ta_95oo.tid              3,135
  ta_95oop_ca.tid
                           3,004
  ta_95over.tid            3,019
  ta_95rectex.tid
                           2,959
  ta_ada95.tid             3,025
  ta_faq.tid               2,369
  ta_logo.tid              2,443
  ta_notes.tid             2,456
  tarte.sid                4,164
  tasking.sid              4,232
  taskit.sid               4,991
  tbd.sid                  4,698
  tcpip.sid                5,220
  tcpip2.sid               5,178
  tdars.sid                4,604
  techxfer.tid             7,524
  tedit.sid                4,752
  telnet.sid               5,197
  testlog.sid              4,789
  tetris_ada.sid           4,775
  tod.sid                  5,037
  tod00.sid                4,716
  toolkit.sid             16,898
  tracker.sid              5,288
  trada.sid                4,813
  trainpl.tid              3,258
  uatl.sid                 5,989
  ufn.sid                  4,746
  unitrep.sid              4,515
  unpage.sid               4,668
  userdocs.mid             4,517
  userif.tid               3,420
  usermeta.tid             2,877
  vaxtape.sid              5,264
  vdt100.sid               4,457
  vhdl                        23
  vhdl.mid                 3,860
  vhdl_93.mid              2,537
  vhdl_anavhdl.mid
                           5,134
  vhdl_cookbook.mid
                           2,656
  vhdl_general.mid
                           3,071
  vhdl_models.mid
                           3,593
  vhdl_packages.mid
                           2,587
  vhdl_tools.mid           3,286
  vhdl_validate.mid
                           8,505
  vstring.sid              4,633
  vt2.sid                  5,095
  wisr.tid                29,633
  wmgs.sid                 4,213
  woodruff.sid            20,927
  wp.sid                   5,159
  x1.sid                   5,152
  x11gnu.sid              11,583
  x1804.sid                5,623
  x2.tid                   3,406
  x3.tid                   3,211
  xanim.sid                4,726
  xmker.sid                4,862
  zen.tid                  3,510


Totals
  ==============  ==============
  568 Files            3,132,441

ABSTRACT

Penelope Reference Manual

     Penelope is an interactive environment that helps its user to
develop and verify programs written in a rich subset of sequential Ada.
Penelope is well-suited to developing programs in the goal-directed
style advocated by Gries and Dijkstra. In this style the programmer
develops a program from a specification in a way that ensures the
program will meet the specification. Of course, Penelope can also be
used to verify previously written programs. Sometimes we have to modify
a completed program. With Penelope, it is often possible to verify a
modified version of a program with minimal effort, by replaying and
modifying the original program's proof.
     This manual documents the language and commands of the Penelope
environment.  It is intended for the Penelope user, who desires to write
specifications, develop programs, and carry out correctness proofs using
Penelope. The user is assumed to be an Ada programmer with a strong
mathematical background. A working knowledge of predicate calculus is
essential. Even with such a background, the user may require the
assistance of a trained mathematician for the more demanding aspects of
Penelope, notably providing consistent axiomatic definitions of
functions used in the specifications, organizing the proofs of the
verification conditions, and proving lemmas needed during the
verification.  Chapter 2 documents how to get Penelope running.  In
order to develop and verify programs using Penelope, though, you will
need to understand Penelope's approach to formal verification and to
simplification and theorem proving.


REVISION HISTORY

STARS-AC-A023/004/00  1 June 94  Initial release to the PAL


RELEASE NOTICE

Approved for public release; Distribution unlimited


DISCLAIMER

This documentation is provided "AS IS" and without any expressed or
implied warranties whatsoever.  No warranties as to performance,
merchantability, or fitness for a particular purpose exist.

The user must assume the entire risk and liability of using this
document.  In no event shall any person or organization of people be
held responsible for any direct, indirect, consequential or
inconsequential damages or lost profits.