rpms/why/devel README.why, NONE, 1.1 README.why-coq.Fedora, NONE, 1.1 README.why-gwhy.Fedora, NONE, 1.1 caduceus.ps, NONE, 1.1 gwhy-2.14.patch, NONE, 1.1 gwhy-icon.png, NONE, 1.1 gwhy.desktop, NONE, 1.1 import.log, NONE, 1.1 min.mlw, NONE, 1.1 min_why.why.result, NONE, 1.1 why-2.14-Makefile.in.patch, NONE, 1.1 why-config.patch, NONE, 1.1 why.spec, NONE, 1.1 .cvsignore, 1.1, 1.2 sources, 1.1, 1.2
Alan Dunn (amdunn)
fedora-extras-commits at redhat.com
Tue Aug 5 16:49:47 UTC 2008
- Previous message (by thread): rpms/gnome-panel/devel .cvsignore, 1.80, 1.81 gnome-panel.spec, 1.311, 1.312 preferred-apps.patch, 1.7, 1.8 sources, 1.83, 1.84 gnome-panel-2.13.5-switch-user.patch, 1.3, NONE gnome-panel-2.19.5-vendor.patch, 1.1, NONE gnome-panel-2.22.0-ck-shutdown.patch, 1.3, NONE gnome-panel-larger-find-window.patch, 1.1, NONE gnome-panel-launch-with-gio.patch, 1.3, NONE gnome-panel-use-gio.patch, 1.1, NONE icon-names.patch, 1.2, NONE timezone-debug.patch, 1.2, NONE
- Next message (by thread): rpms/orca/devel .cvsignore, 1.35, 1.36 orca.spec, 1.57, 1.58 sources, 1.36, 1.37
- Messages sorted by:
[ date ]
[ thread ]
[ subject ]
[ author ]
Author: amdunn
Update of /cvs/pkgs/rpms/why/devel
In directory cvs-int.fedora.redhat.com:/tmp/cvs-serv25765/devel
Modified Files:
.cvsignore sources
Added Files:
README.why README.why-coq.Fedora README.why-gwhy.Fedora
caduceus.ps gwhy-2.14.patch gwhy-icon.png gwhy.desktop
import.log min.mlw min_why.why.result
why-2.14-Makefile.in.patch why-config.patch why.spec
Log Message:
Initial commit of Fedora why package.
--- NEW FILE README.why ---
Fedora why package:
Contains the main why executable and supporting tools.
Consider visiting the main Why site - http://why.lri.fr - for more
documentation. Also, there is more information about the tools
Caduceus and Krakatoa at http://caduceus.lri.fr and
http://krakatoa.lri.fr respectively.
--- NEW FILE README.why-coq.Fedora ---
Fedora why-coq package:
Contains libraries for interfacing why with Coq.
You shouldn't have to do anything extra - you should now just be able
to use the Coq-related capabilities of Why.
--- NEW FILE README.why-gwhy.Fedora ---
Fedora why-gwhy package:
Contains the gwhy GUI for Why.
Run gwhy with "gwhy <filename>". (If you forget and run without a
filename you'll be prompted for it.)
--- NEW FILE caduceus.ps ---
%!PS-Adobe-2.0
%%Creator: dvips(k) 5.95a Copyright 2005 Radical Eye Software
%%Title: caduceus.dvi
%%Pages: 34
%%PageOrder: Ascend
%%BoundingBox: 0 0 595 842
%%DocumentFonts: CMSS17 CMR12 CMTI12 CMTT12 CMBX12 CMSS12 CMSY10
%%+ CMSSBX10 CMTT10 CMMI12 CMITT10 CMBXTI10 CMSL12 CMMI8 CMR8 CMSY8
%%DocumentPaperSizes: a4
%%EndComments
%DVIPSWebPage: (www.radicaleye.com)
%DVIPSCommandLine: dvips caduceus.dvi -o caduceus.ps
%DVIPSParameters: dpi=600
%DVIPSSource: TeX output 2008.07.28:1403
%%BeginProcSet: tex.pro 0 0
%!
/TeXDict 300 dict def TeXDict begin/N{def}def/B{bind def}N/S{exch}N/X{S
N}B/A{dup}B/TR{translate}N/isls false N/vsize 11 72 mul N/hsize 8.5 72
mul N/landplus90{false}def/@rigin{isls{[0 landplus90{1 -1}{-1 1}ifelse 0
0 0]concat}if 72 Resolution div 72 VResolution div neg scale isls{
landplus90{VResolution 72 div vsize mul 0 exch}{Resolution -72 div hsize
mul 0}ifelse TR}if Resolution VResolution vsize -72 div 1 add mul TR[
matrix currentmatrix{A A round sub abs 0.00001 lt{round}if}forall round
exch round exch]setmatrix}N/@landscape{/isls true N}B/@manualfeed{
statusdict/manualfeed true put}B/@copies{/#copies X}B/FMat[1 0 0 -1 0 0]
N/FBB[0 0 0 0]N/nn 0 N/IEn 0 N/ctr 0 N/df-tail{/nn 8 dict N nn begin
/FontType 3 N/FontMatrix fntrx N/FontBBox FBB N string/base X array
/BitMaps X/BuildChar{CharBuilder}N/Encoding IEn N end A{/foo setfont}2
array copy cvx N load 0 nn put/ctr 0 N[}B/sf 0 N/df{/sf 1 N/fntrx FMat N
df-tail}B/dfs{div/sf X/fntrx[sf 0 0 sf neg 0 0]N df-tail}B/E{pop nn A
definefont setfont}B/Cw{Cd A length 5 sub get}B/Ch{Cd A length 4 sub get
}B/Cx{128 Cd A length 3 sub get sub}B/Cy{Cd A length 2 sub get 127 sub}
B/Cdx{Cd A length 1 sub get}B/Ci{Cd A type/stringtype ne{ctr get/ctr ctr
1 add N}if}B/CharBuilder{save 3 1 roll S A/base get 2 index get S
/BitMaps get S get/Cd X pop/ctr 0 N Cdx 0 Cx Cy Ch sub Cx Cw add Cy
setcachedevice Cw Ch true[1 0 0 -1 -.1 Cx sub Cy .1 sub]{Ci}imagemask
restore}B/D{/cc X A type/stringtype ne{]}if nn/base get cc ctr put nn
/BitMaps get S ctr S sf 1 ne{A A length 1 sub A 2 index S get sf div put
}if put/ctr ctr 1 add N}B/I{cc 1 add D}B/bop{userdict/bop-hook known{
bop-hook}if/SI save N @rigin 0 0 moveto/V matrix currentmatrix A 1 get A
mul exch 0 get A mul add .99 lt{/QV}{/RV}ifelse load def pop pop}N/eop{
SI restore userdict/eop-hook known{eop-hook}if showpage}N/@start{
userdict/start-hook known{start-hook}if pop/VResolution X/Resolution X
1000 div/DVImag X/IEn 256 array N 2 string 0 1 255{IEn S A 360 add 36 4
index cvrs cvn put}for pop 65781.76 div/vsize X 65781.76 div/hsize X}N
/p{show}N/RMat[1 0 0 -1 0 0]N/BDot 260 string N/Rx 0 N/Ry 0 N/V{}B/RV/v{
/Ry X/Rx X V}B statusdict begin/product where{pop false[(Display)(NeXT)
(LaserWriter 16/600)]{A length product length le{A length product exch 0
exch getinterval eq{pop true exit}if}{pop}ifelse}forall}{false}ifelse
end{{gsave TR -.1 .1 TR 1 1 scale Rx Ry false RMat{BDot}imagemask
grestore}}{{gsave TR -.1 .1 TR Rx Ry scale 1 1 false RMat{BDot}
imagemask grestore}}ifelse B/QV{gsave newpath transform round exch round
exch itransform moveto Rx 0 rlineto 0 Ry neg rlineto Rx neg 0 rlineto
fill grestore}B/a{moveto}B/delta 0 N/tail{A/delta X 0 rmoveto}B/M{S p
delta add tail}B/b{S p tail}B/c{-4 M}B/d{-3 M}B/e{-2 M}B/f{-1 M}B/g{0 M}
B/h{1 M}B/i{2 M}B/j{3 M}B/k{4 M}B/w{0 rmoveto}B/l{p -4 w}B/m{p -3 w}B/n{
p -2 w}B/o{p -1 w}B/q{p 1 w}B/r{p 2 w}B/s{p 3 w}B/t{p 4 w}B/x{0 S
rmoveto}B/y{3 2 roll p a}B/bos{/SS save N}B/eos{SS restore}B end
%%EndProcSet
%%BeginProcSet: texps.pro 0 0
%!
TeXDict begin/rf{findfont dup length 1 add dict begin{1 index/FID ne 2
index/UniqueID ne and{def}{pop pop}ifelse}forall[1 index 0 6 -1 roll
exec 0 exch 5 -1 roll VResolution Resolution div mul neg 0 0]FontType 0
ne{/Metrics exch def dict begin Encoding{exch dup type/integertype ne{
pop pop 1 sub dup 0 le{pop}{[}ifelse}{FontMatrix 0 get div Metrics 0 get
div def}ifelse}forall Metrics/Metrics currentdict end def}{{1 index type
/nametype eq{exit}if exch pop}loop}ifelse[2 index currentdict end
definefont 3 -1 roll makefont/setfont cvx]cvx def}def/ObliqueSlant{dup
sin S cos div neg}B/SlantFont{4 index mul add}def/ExtendFont{3 -1 roll
mul exch}def/ReEncodeFont{CharStrings rcheck{/Encoding false def dup[
exch{dup CharStrings exch known not{pop/.notdef/Encoding true def}if}
forall Encoding{]exch pop}{cleartomark}ifelse}if/Encoding exch def}def
end
%%EndProcSet
%%BeginFont: CMSY8
%!PS-AdobeFont-1.1: CMSY8 1.0
%%CreationDate: 1991 Aug 15 07:22:10
% Copyright (C) 1997 American Mathematical Society. All Rights Reserved.
11 dict begin
/FontInfo 7 dict dup begin
/version (1.0) readonly def
/Notice (Copyright (C) 1997 American Mathematical Society. All Rights Reserved) readonly def
/FullName (CMSY8) readonly def
/FamilyName (Computer Modern) readonly def
/Weight (Medium) readonly def
/ItalicAngle -14.035 def
/isFixedPitch false def
end readonly def
/FontName /CMSY8 def
/PaintType 0 def
/FontType 1 def
/FontMatrix [0.001 0 0 0.001 0 0] readonly def
/Encoding 256 array
0 1 255 {1 index exch /.notdef put} for
dup 24 /similar put
readonly def
/FontBBox{-30 -955 1185 779}readonly def
currentdict end
currentfile eexec
D9D66F633B846A97B686A97E45A3D0AA052F09F9C8ADE9D907C058B87E9B6964
7D53359E51216774A4EAA1E2B58EC3176BD1184A633B951372B4198D4E8C5EF4
A213ACB58AA0A658908035BF2ED8531779838A960DFE2B27EA49C37156989C85
E21B3ABF72E39A89232CD9F4237FC80C9E64E8425AA3BEF7DED60B122A52922A
221A37D9A807DD01161779DDE7D5FC1B2109839E5B52DFBB2A7C1B5D8E7E8AA0
5B10EA43D6A8ED61AF5B23D49920D8F79DAB6A59062134D84AC0100187A6CD1F
80F5DDD9D222ACB1C23326A7656A635C4A241CCD32CBFDF8363206B8AA36E107
1477F5496111E055C7491002AFF272E46ECC46422F0380D093284870022523FB
DA1716CC4F2E2CCAD5F173FCBE6EDDB874AD255CD5E5C0F86214393FCB5F5C20
9C3C2BB5886E36FC3CCC21483C3AC193485A46E9D22BD7201894E4D45ADD9BF1
CC5CF6A5010B5654AC0BE0DA903DB563B13840BA3015F72E51E3BC80156388BA
F83C7D393392BCBC227771CDCB976E93302531886DDA73EBC9178917EFD0C20B
133F1E59B85B951BFD0F316B8388A2B2F592AA8E397A5B9CAFF5B4CCE4E1ADD2
8F729F0630732D4847C362E272B7274624E188C85105E7C0B37C096366921267
41C3DCD5E3194BAD5DA807DA08810290990701CAAD643AB9A793EF22CB865D45
BADB87571029B4B85A545C09B0F3E0DD97A0D5673CC1D8AED65357D61646BA67
9F9172720B0C2D107750D0FD31C3305C396C48712765D1980AA17A6DABD218F8
AB60564557F8AD2B5B983053A1C10D7CA4CE0781E4BE737CA9E83857A5340C3F
996669660C962C501FD8DC9630813069A707765416E0D313DBC78B270062B7DD
D24C558E60B24E6FD88FD1845FCC19171D579F9C6AA3784BC6B82427EA25AE51
E413B0B3B026
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
0000000000000000000000000000000000000000000000000000000000000000
cleartomark
%%EndFont
%%BeginFont: CMR8
%!PS-AdobeFont-1.1: CMR8 1.0
%%CreationDate: 1991 Aug 20 16:39:40
% Copyright (C) 1997 American Mathematical Society. All Rights Reserved.
11 dict begin
/FontInfo 7 dict dup begin
/version (1.0) readonly def
/Notice (Copyright (C) 1997 American Mathematical Society. All Rights Reserved) readonly def
/FullName (CMR8) readonly def
/FamilyName (Computer Modern) readonly def
/Weight (Medium) readonly def
/ItalicAngle 0 def
/isFixedPitch false def
end readonly def
/FontName /CMR8 def
/PaintType 0 def
/FontType 1 def
/FontMatrix [0.001 0 0 0.001 0 0] readonly def
/Encoding 256 array
0 1 255 {1 index exch /.notdef put} for
dup 43 /plus put
dup 49 /one put
dup 50 /two put
readonly def
/FontBBox{-36 -250 1070 750}readonly def
currentdict end
currentfile eexec
D9D66F633B846A97B686A97E45A3D0AA052A014267B7904EB3C0D3BD0B83D891
016CA6CA4B712ADEB258FAAB9A130EE605E61F77FC1B738ABC7C51CD46EF8171
9098D5FEE67660E69A7AB91B58F29A4D79E57022F783EB0FBBB6D4F4EC35014F
D2DECBA99459A4C59DF0C6EBA150284454E707DC2100C15B76B4C19B84363758
469A6C558785B226332152109871A9883487DD7710949204DDCF837E6A8708B8
2BDBF16FBC7512FAA308A093FE5CF4E9D2405B169CD5365D6ECED5D768D66D6C
68618B8C482B341F8CA38E9BB9BAFCFAAD9C2F3FD033B62690986ED43D9C9361
3645B82392D5CAE11A7CB49D7E2E82DCD485CBA1772CE422BB1D7283AD675B65
48A7EA0069A883EC1DAA3E1F9ECE7586D6CF0A128CD557C7E5D7AA3EA97EBAD3
9619D1BFCF4A6D64768741EDEA0A5B0EFBBF347CDCBE2E03D756967A16B613DB
0FC45FA2A3312E0C46A5FD0466AB097C58FFEEC40601B8395E52775D0AFCD7DB
8AB317333110531E5C44A4CB4B5ACD571A1A60960B15E450948A5EEA14DD330F
EA209265DB8E1A1FC80DCD3860323FD26C113B041A88C88A21655878680A4466
FA10403D24BB97152A49B842C180E4D258C9D48F21D057782D90623116830BA3
9902B3C5F2F2DD01433B0D7099C07DBDE268D0FFED5169BCD03D48B2F058AD62
D8678C626DC7A3F352152C99BA963EF95F8AD11DB8B0D351210A17E4C2C55AD8
9EB64172935D3C20A398F3EEEEC31551966A7438EF3FEE422C6D4E05337620D5
ACC7B52BED984BFAAD36EF9D20748B05D07BE4414A63975125D272FAD83F76E6
10FFF8363014BE526D580873C5A42B70FA911EC7B86905F13AFE55EB0273F582
83158793B8CC296B8DE1DCCF1250FD57CB0E035C7EDA3B0092ED940D37A05493
2EC54E09B984FCA4AB7D2EA182BCF1263AA244B07EC0EA901C077A059F709F30
4384CB5FA748F2054FAD9A7A43D4EA427918BD414F766531136B60C3477C6632
BEFE3897B58C19276A301926C2AEF2756B367319772C9B201C49B4D935A8267B
041D6F1783B6AEA4DAC4F5B3507D7032AA640AAB12E343A4E9BDCF419C04A721
3888B25AF4E293AACED9A6BDC78E61DA1C424C6503CC1885F762BFD4563ABA4F
D926227FAD2B2D4975835541F5A97E7A70F5CB40266CB9B4E609B94B31263442
35FBADB202B4032E1C3165F83176413544AECC056C371F4B41C04121C4D20A7A
CE519F46C3999F58F5F43BF799D624FDF62A229D8B9189CF5AFAE6141FF16B53
BB2B3EE9FB2467181C50CD8F8F32BC6609385D9D111EE2A589687D84C6C2FB75
A48CDD9A85F106AB9D3F906105C56CD993793C20FC7E5202428340F3DD4F10DB
561A3958B4CD377D1B833D27F6F9F233CB9D99F95309D20134DD6A47A5291D43
E49BF013864BA87ED38FB9755A8077105EDF397023D0C1A1B21B951AB1A4FFA2
72990283B3B455447DA9E68C7CE660F8BCC18F5FD82371D89BBB363EA0FDA552
3059558108DEC9D2E6BED7BDD5C0243485F642DAF3B3A719E098D25B24E2D1F7
9B9DE8CAD714415F9DC0F0A7BF618BE0FBD81618CAA161548B2038163020318F
18C088D44BEFB4397412661EA87CE38799B3AAEE28A008A3FF638C665DE01D88
1604BA57E90D82855317F1A99B9C6FE3E6B46F5EEC32DAA013BB124E6701FDBB
821E8527C2BD04E8D9770BB5037793DC4DFE6CBFB2F0850B29BE67083451B071
413B07804AD37CA3AAD6D799091E5ABB2F5C55FDD77C4E421D4070EAB055C3CD
[...4953 lines suppressed...]
(et)h(supp)s(orted)f(b)m(y)j Fp(Caduceus)e Ft(but)f(will)h(b)s(e)f(so)g
(in)g(future)h(v)m(ersions)0 3587 y(of)k(the)h(to)s(ol:)145
3790 y Fn(\017)49 b Ft(standard)33 b(library)g(functions:)44
b Fr(memcpy)p Ft(,)35 b Fr(strcmp)p Ft(,)f(etc.)0 4079
y Fo(2.6.2)136 b(Other)45 b(unsupp)t(orted)f(features)0
4264 y Ft(The)34 b(follo)m(wing)e(features)i(are)e(not)h(planed)g(to)f
(b)s(e)h(supp)s(orted)h(b)m(y)g Fp(Caduceus)p Ft(:)145
4467 y Fn(\017)49 b Ft(arbitrary)34 b Fr(goto)f Ft(\(some)h(simple)g
Fr(goto)p Ft('s)g(are)f(supp)s(orted\))145 4671 y Fn(\017)49
b Ft(function)25 b(p)s(oin)m(ter)f(\(apart)g(from)g(trivial)h
(situations)g(where)h(w)m(e)f(kno)m(w)g(at)f(compile-time)i(whic)m(h)
244 4791 y(function)33 b(is)g(p)s(oin)m(ted)g(at\))145
4995 y Fn(\017)49 b Ft(p)s(oin)m(ter)34 b(cast)h(\(e.g.)47
b(casting)35 b(an)e Fr(int*)i Ft(to)f(a)f Fr(void*)p
Ft(,)j(passing)f(it)f(to)f(a)h(function)g(whic)m(h)i(casts)244
5115 y(it)c(bac)m(k)i(to)e Fr(int*)p Ft(\))145 5318 y
Fn(\017)49 b Ft(an)m(y)33 b(non-ANSI)g(feature)1832 5816
y(29)p eop end
%%Page: 30 30
TeXDict begin 30 29 bop 1832 5816 a Ft(30)p eop end
%%Page: 31 31
TeXDict begin 31 30 bop 0 764 a Fq(Bibliograph)-6 b(y)49
1217 y Ft([1])49 b(CV)m(C)33 b(Lite.)44 b Fr(http://verify.stanford.ed)
q(u/CV)q(CL/)q Ft(.)49 1421 y([2])49 b(ESC/Ja)m(v)-5
b(a2.)43 b Fr(http://www.sos.cs.ru.nl)q(/res)q(earc)q(h/es)q(cja)q(va)p
Ft(.)49 1625 y([3])49 b(HOL)32 b(4.)43 b Fr(http://hol.sourceforge.ne)q
(t/)p Ft(.)49 1829 y([4])49 b(HOL)32 b(Ligh)m(t.)44 b
Fr(http://www.cl.cam.ac.uk/use)q(rs/)q(jrh/)q(hol-)5
b(lig)q(ht/)p Ft(.)49 2033 y([5])49 b(Isab)s(elle/HOL.)44
b Fr(http://isabelle.in.tum.de/)q Ft(.)49 2237 y([6])49
b(Mizar.)43 b Fr(http://mizar.uwb.edu.pl)q(/)p Ft(.)49
2442 y([7])49 b(The)33 b(Co)s(q)g(Pro)s(of)f(Assistan)m(t.)45
b Fr(http://coq.inria.fr/)p Ft(.)49 2646 y([8])k(The)33
b(haR)-11 b(V)j(ey)33 b(decision)h(pro)s(cedure.)45 b
Fr(http://www.loria.fr/)2637 2620 y Fa(\030)2697 2646
y Fr(ranise/haRVey/)p Ft(.)49 2850 y([9])k(The)33 b(Ob)5
b(jectiv)m(e)35 b(Caml)e(language.)43 b Fr(http://caml.inria.fr/)p
Ft(.)0 3054 y([10])49 b(The)33 b(PVS)g(Sp)s(eci\014cation)h(and)f(V)-8
b(eri\014cation)33 b(System.)45 b Fr(http://pvs.csl.sri.com/)p
Ft(.)0 3258 y([11])k(The)87 b(Simplify)g(decision)h(pro)s(cedure.)204
b Fr(http://research.compaq.c)q(om/)q(SRC/)q(esc/)201
3379 y(simplify/)p Ft(.)0 3583 y([12])49 b(The)33 b(Wh)m(y)h(v)m
(eri\014cation)g(to)s(ol.)42 b Fr(http://why.lri.fr/)p
Ft(.)0 3787 y([13])49 b(Ric)m(hard)35 b(Bornat.)50 b(Pro)m(ving)36
b(p)s(oin)m(ter)f(programs)g(in)g(Hoare)g(logic.)50 b(In)35
b Fs(Mathematics)i(of)g(Pr)-5 b(o-)201 3907 y(gr)g(am)34
b(Construction)p Ft(,)e(pages)h(102{126,)e(2000.)0 4112
y([14])49 b(Ro)s(d)28 b(Burstall.)39 b(Some)30 b(tec)m(hniques)j(for)c
(pro)m(ving)h(correctness)i(of)d(programs)g(whic)m(h)i(alter)f(data)201
4232 y(structures.)45 b Fs(Machine)34 b(Intel)5 b(ligenc)-5
b(e)p Ft(,)31 b(7:23{50,)g(72.)0 4436 y([15])49 b(P)m(atrice)c(Chalin.)
81 b(Reassessing)47 b(JML's)f(logical)f(foundation.)80
b(In)45 b Fs(Pr)-5 b(o)g(c)g(e)g(e)g(dings)45 b(of)g(the)i(7th)201
4556 y(Workshop)28 b(on)h(F)-7 b(ormal)27 b(T)-7 b(e)i(chniques)28
b(for)g(Java-like)g(Pr)-5 b(o)g(gr)g(ams)29 b(\(FTfJP'05\))p
Ft(,)d(Glasgo)m(w,)i(Scot-)201 4677 y(land,)k(July)i(2005.)0
4881 y([16])49 b(P)m(atrice)38 b(Chalin.)57 b(A)37 b(sound)h(assertion)
g(seman)m(tics)h(for)e(the)g(dep)s(endable)i(systems)g(ev)m(olution)201
5001 y(v)m(erifying)c(compiler.)49 b(In)35 b Fs(Pr)-5
b(o)g(c)g(e)g(e)g(dings)35 b(of)h(the)g(International)f(Confer)-5
b(enc)g(e)35 b(on)h(Softwar)-5 b(e)36 b(En-)201 5122
y(gine)-5 b(ering)36 b(\(ICSE'07\))p Ft(,)g(pages)h(23{33,)f(Los)g
(Alamitos,)h(CA,)g(USA,)g(2007.)e(IEEE)i(Computer)201
5242 y(So)s(ciet)m(y)-8 b(.)0 5446 y([17])49 b(Claude)43
b(Marc)m(h)m(\023)-46 b(e,)46 b(Christine)e(P)m(aulin)g(and)e(Xa)m
(vier)i(Urbain.)73 b(The)43 b(Krak)-5 b(atoa)41 b(to)s(ol.)72
b Fr(http:)201 5567 y(//krakatoa.lri.fr/)p Ft(.)1832
5816 y(31)p eop end
%%Page: 32 32
TeXDict begin 32 31 bop 0 100 a Ft([18])49 b(Brian)c(Kernighan)g(and)h
(Dennis)g(Ritc)m(hie.)82 b Fs(The)46 b(C)h(Pr)-5 b(o)g(gr)g(amming)45
b(L)-5 b(anguage)46 b(\(2nd)g(Ed.\))p Ft(.)201 220 y(Pren)m(tice-Hall,)
34 b(1988.)0 423 y([19])49 b(Gary)33 b(T.)h(Lea)m(v)m(ens,)h(Alb)s(ert)
f(L.)f(Bak)m(er,)i(and)f(Clyde)h(Rub)m(y)-8 b(.)46 b(Preliminary)35
b(design)g(of)e(JML:)h(A)201 544 y(b)s(eha)m(vioral)j(in)m(terface)g
(sp)s(eci\014cation)h(language)e(for)g(Ja)m(v)-5 b(a.)54
b(T)-8 b(ec)m(hnical)39 b(Rep)s(ort)d(98-06i,)g(Io)m(w)m(a)201
664 y(State)c(Univ)m(ersit)m(y)-8 b(,)35 b(2000.)0 868
y([20])49 b(Gary)33 b(T.)h(Lea)m(v)m(ens,)h(Alb)s(ert)f(L.)f(Bak)m(er,)
i(and)f(Clyde)h(Rub)m(y)-8 b(.)46 b(Preliminary)35 b(design)g(of)e
(JML:)h(A)201 988 y(b)s(eha)m(vioral)j(in)m(terface)g(sp)s
(eci\014cation)h(language)e(for)g(Ja)m(v)-5 b(a.)54 b(T)-8
b(ec)m(hnical)39 b(Rep)s(ort)d(98-06i,)g(Io)m(w)m(a)201
1108 y(State)c(Univ)m(ersit)m(y)-8 b(,)35 b(2000.)1832
5816 y(32)p eop end
%%Page: 33 33
TeXDict begin 33 32 bop 0 764 a Fq(Con)-6 b(ten)g(ts)0
1314 y Fh(F)d(orew)m(ord)3249 b(3)0 1532 y(1)90 b(T)-9
b(utorial)3166 b(5)146 1652 y Ft(1.1)100 b(Basic)33 b(use)h(of)39
b Fp(Caduceus)33 b Ft(.)50 b(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)
g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)199
b(5)146 1773 y(1.2)100 b(P)m(oin)m(ter)33 b(access)i(and)d(mo)s
(di\014cation)75 b(.)50 b(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)g
(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)199 b(7)146
1893 y(1.3)100 b(Arra)m(ys)62 b(.)50 b(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g
(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)
g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)199 b(9)371 2013
y(1.3.1)111 b(Arra)m(y)33 b(indexing)88 b(.)50 b(.)g(.)g(.)g(.)g(.)g(.)
g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g
(.)g(.)g(.)g(.)199 b(9)371 2134 y(1.3.2)111 b(Arra)m(ys)33
b(and)g(lo)s(ops)76 b(.)50 b(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)
g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)150
b(11)146 2254 y(1.4)100 b(Structures)62 b(.)50 b(.)g(.)g(.)g(.)f(.)h(.)
g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)g
(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)150 b(12)146
2374 y(1.5)100 b(Calling)33 b(functions)85 b(.)49 b(.)h(.)g(.)g(.)g(.)g
(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)
h(.)g(.)g(.)g(.)g(.)g(.)g(.)150 b(14)146 2495 y(1.6)100
b(A)32 b(complete)i(example)96 b(.)50 b(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g
(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)
g(.)g(.)150 b(16)146 2615 y(1.7)100 b(Other)33 b(features)g(not)f
(already)h(in)g(the)g(tutorial)40 b(.)50 b(.)g(.)g(.)g(.)g(.)g(.)g(.)g
(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)150 b(16)371 2736
y(1.7.1)111 b(Other)33 b(annotations)99 b(.)50 b(.)g(.)g(.)g(.)g(.)g(.)
f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g
(.)g(.)150 b(16)371 2856 y(1.7.2)111 b(Logical)32 b(declarations)i(.)50
b(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f
(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)150 b(18)371 2976 y(1.7.3)111
b(In)m(v)-5 b(arian)m(t)33 b(declarations)e(.)50 b(.)g(.)g(.)g(.)g(.)f
(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)
g(.)150 b(20)0 3194 y Fh(2)90 b(Reference)38 b(man)m(ual)2632
b(21)146 3315 y Ft(2.1)100 b(Command)33 b(line)g(options)74
b(.)50 b(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)
g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)150 b(21)146
3435 y(2.2)100 b(Input)33 b(Files)g(Syn)m(tax)90 b(.)50
b(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g
(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)150 b(23)371
3555 y(2.2.1)111 b(Lexical)33 b(con)m(v)m(en)m(tions)55
b(.)50 b(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)
g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)150 b(23)371 3676
y(2.2.2)111 b(Syn)m(tax)48 b(.)i(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)
g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g
(.)g(.)g(.)g(.)g(.)150 b(23)146 3796 y(2.3)100 b(Arithmetic)38
b(.)50 b(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)
h(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g
(.)150 b(23)371 3917 y(2.3.1)111 b(In)m(teger)33 b(arithmetic)i(.)50
b(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g
(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)150 b(23)371 4037
y(2.3.2)111 b(En)m(umeration)34 b(t)m(yp)s(es)72 b(.)50
b(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f
(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)150 b(26)371 4157 y(2.3.3)111
b(Floating-p)s(oin)m(t)31 b(arithmetic)f(.)50 b(.)g(.)g(.)f(.)h(.)g(.)g
(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)150
b(27)146 4278 y(2.4)100 b(Memory)33 b(mo)s(del)g(and)g(p)s(oin)m(ter)g
(arithmetic)92 b(.)50 b(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g
(.)g(.)g(.)g(.)g(.)g(.)150 b(28)146 4398 y(2.5)100 b(Memory)33
b(allo)s(cation)85 b(.)50 b(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h
(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)
150 b(29)146 4518 y(2.6)100 b(Unsupp)s(orted)33 b(features)43
b(.)50 b(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)
g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)150 b(29)371
4639 y(2.6.1)111 b(F)-8 b(eatures)33 b(not)f(supp)s(orted)i(in)f
(curren)m(t)g(v)m(ersion)d(.)50 b(.)g(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g
(.)g(.)g(.)g(.)150 b(29)371 4759 y(2.6.2)111 b(Other)33
b(unsupp)s(orted)h(features)83 b(.)50 b(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g
(.)g(.)g(.)g(.)f(.)h(.)g(.)g(.)g(.)g(.)g(.)g(.)150 b(29)0
4977 y Fh(Index)3373 b(33)1832 5816 y Ft(33)p eop end
%%Page: 34 34
TeXDict begin 34 33 bop 0 559 a Fq(Index)0 990 y Fr(#)p
Ft(,)33 b(9)0 1198 y(Aliasing,)g(15)0 1319 y(Annotations,)g(23)0
1439 y Fd(arith)p 212 1439 30 4 v 35 w(op)p Ft(,)g(grammar)f(en)m(try)
-8 b(,)34 b(25)0 1560 y(Arithmetic,)g(23)0 1680 y Fr(assert)p
Ft(,)g(17,)e(24)0 1801 y Fr(assigns)p Ft(,)i(14,)f(15,)f(24)0
1922 y Fr(axiom)p Ft(,)i(18,)e(24)0 2129 y Fp(Caduceus)p
Ft(,)i(3,)e(5,)h(7{10,)e(13,)i(15,)f(21,)g(27{29)0 2250
y Fr(check-enum)p Ft(,)j(26)0 2371 y Fd(constan)m(t)p
Ft(,)f(grammar)e(en)m(try)-8 b(,)34 b(25)0 2491 y Fp(Co)s(q)p
Ft(,)e(5,)h(6,)f(8,)h(22,)f(27)0 2699 y Fr(decreases)p
Ft(,)j(24)0 2907 y Fr(ensures)p Ft(,)f(5,)f(24)0 3027
y(En)m(umeration,)h(26)0 3235 y(Floating-p)s(oin)m(t)e(arithmetic,)h
(27)0 3356 y Fr(\\forall)p Ft(,)h(11)0 3476 y Fr(\\fresh)p
Ft(,)g(25)0 3684 y Fr(ghost)p Ft(,)g(24)0 3892 y Fr(-int-model)p
Ft(,)h(23)0 4012 y Fr(invariant)p Ft(,)g(11,)d(20,)g(24)0
4220 y Fr(label)p Ft(,)i(17,)e(24)0 4341 y(Lexical)i(con)m(v)m(en)m
(tions)166 4461 y(C)f(programs,)g(23)0 4582 y Fr(logic)p
Ft(,)h(18,)e(24)0 4789 y Fr(\\max)p 210 4789 31 4 v 38
w(range)p Ft(,)i(26)0 4910 y Fr(memory)p Ft(,)g(9)0 5031
y Fr(\\min)p 210 5031 V 38 w(range)p Ft(,)g(26)0 5238
y Fr(\\old)p Ft(,)g(10)0 5359 y(Option,)f(of)f(the)h(command)g(line,)h
(21)0 5567 y(P)m(oin)m(ter)g(aliasing,)f(15)1922 990
y(P)m(oin)m(ter)h(arithmetic,)f(28)1922 1111 y Fd(predicate)p
Ft(,)h(grammar)e(en)m(try)-8 b(,)34 b(25)1922 1231 y
Fr(predicate)p Ft(,)h(13,)d(24)1922 1351 y Fp(PVS)p Ft(,)h(7)1922
1555 y Fd(relation)p Ft(,)g(grammar)f(en)m(try)-8 b(,)34
b(25)1922 1675 y Fr(requires)p Ft(,)h(8,)d(24)1922 1796
y Fr(\\result)p Ft(,)i(5)1922 1999 y Fr(set)p Ft(,)f(24)1922
2119 y Fr(shift)p Ft(,)h(10)1922 2240 y Fp(Simplify)p
Ft(,)e(6{8)1922 2360 y Fd(sym)m(b)s(ol)p Ft(,)i(grammar)e(en)m(try)-8
b(,)34 b(25)1922 2481 y(Syn)m(tax)g(\(of)e(input)h(\014les\),)h(23)1922
2684 y Fd(term)p Ft(,)f(grammar)f(en)m(try)-8 b(,)34
b(25)1922 2887 y Fr(upd)p Ft(,)f(9)1922 3091 y Fr(\\valid)p
Ft(,)h(8)1922 3211 y Fr(\\valid)p Ft(,)g(25)1922 3331
y Fr(\\valid)p 2234 3331 V 38 w(index)p Ft(,)g(10,)e(25)1922
3452 y Fr(\\valid)p 2234 3452 V 38 w(range)p Ft(,)i(11,)e(25)1922
3572 y Fr(variant)p Ft(,)i(11,)e(24)1832 5816 y(34)p
eop end
%%Trailer
userdict /end-hook known{end-hook}if
%%EOF
gwhy-2.14.patch:
--- NEW FILE gwhy-2.14.patch ---
--- bin/gwhy.sh 2008-07-28 08:03:03.000000000 -0400
+++ bin/gwhy.sh 2008-08-01 22:56:01.000000000 -0400
@@ -1,27 +1,40 @@
#!/bin/sh
-case $1 in
+if ! test $1; then
+file=`zenity --file-selection --title="Select the file you want to open with gwhy"`;
+else
+file=$1
+fi
+
+d=`dirname $file`
+cd $d
+
+case $file in
*.java)
- b=`basename $1 .java`
- krakatoa $1 || exit 1
+ b=`basename $file .java`
+ krakatoa $b.java || exit 1
jessie -locs $b.jloc -why-opt -split-user-conj $b.jc || exit 2
make -f $b.makefile gui
;;
*.c)
- b=`basename $1 .c`
- caduceus -why-opt -split-user-conj $1 || exit 1
+ b=`basename $file .c`
+ caduceus -why-opt -split-user-conj $b.c
make -f $b.makefile gui
;;
*.jc)
- b=`basename $1 .jc`
+ b=`basename $file .jc`
jessie $b.jc || exit 1
make -f $b.makefile gui
;;
*.mlw|*.why)
- gwhy-bin -split-user-conj $1
+ b=`basename $file`
+ gwhy-bin -split-user-conj $b
+ ;;
+ ?*)
+ echo "$file does not have file type extension recognized by gwhy"
;;
*)
- echo "don't know what to do with $1"
+ echo "gwhy needs the name of a file to inspect in order to run"
esac
--- NEW FILE gwhy.desktop ---
[Desktop Entry]
Encoding=UTF-8
Name=gwhy
Comment=Examine and develop Why .why files
Exec=gwhy
Icon=ICON-LOCATION-BASE/gwhy-icon.png
Type=Application
Categories=Development;
--- NEW FILE import.log ---
why-2_14-2_fc9:HEAD:why-2.14-2.fc9.src.rpm:1217954050
--- NEW FILE min.mlw ---
logic min: int, int -> int
axiom min_ax: forall x,y:int. min(x,y) <= x
parameter r: int ref
let f (n:int) = {} r := min !r n { r <= r@ }
--- NEW FILE min_why.why.result ---
logic eq_unit : unit, unit -> prop
logic neq_unit : unit, unit -> prop
logic eq_bool : bool, bool -> prop
logic neq_bool : bool, bool -> prop
logic bool_and : bool, bool -> bool
logic bool_or : bool, bool -> bool
logic bool_xor : bool, bool -> bool
logic bool_not : bool -> bool
axiom bool_and_def:
(forall a:bool.
(forall b:bool.
((bool_and(a, b) = true) <-> ((a = true) and (b = true)))))
axiom bool_or_def:
(forall a:bool.
(forall b:bool. ((bool_or(a, b) = true) <-> ((a = true) or (b = true)))))
axiom bool_xor_def:
(forall a:bool. (forall b:bool. ((bool_xor(a, b) = true) <-> (a <> b))))
axiom bool_not_def: (forall a:bool. ((bool_not(a) = true) <-> (a = false)))
logic ite : bool, 'a1, 'a1 -> 'a1
axiom ite_true: (forall x:'a1. (forall y:'a1. (ite(true, x, y) = x)))
axiom ite_false: (forall x:'a1. (forall y:'a1. (ite(false, x, y) = y)))
logic add_int : int, int -> int
logic sub_int : int, int -> int
logic mul_int : int, int -> int
logic div_int : int, int -> int
logic mod_int : int, int -> int
logic neg_int : int -> int
logic lt_int : int, int -> prop
logic le_int : int, int -> prop
logic gt_int : int, int -> prop
logic ge_int : int, int -> prop
logic eq_int : int, int -> prop
logic neq_int : int, int -> prop
logic lt_int_bool : int, int -> bool
logic le_int_bool : int, int -> bool
logic gt_int_bool : int, int -> bool
logic ge_int_bool : int, int -> bool
logic eq_int_bool : int, int -> bool
logic neq_int_bool : int, int -> bool
axiom lt_int_bool_axiom:
(forall x:int. (forall y:int. ((lt_int_bool(x, y) = true) <-> (x < y))))
axiom le_int_bool_axiom:
(forall x:int. (forall y:int. ((le_int_bool(x, y) = true) <-> (x <= y))))
axiom gt_int_bool_axiom:
(forall x:int. (forall y:int. ((gt_int_bool(x, y) = true) <-> (x > y))))
axiom ge_int_bool_axiom:
(forall x:int. (forall y:int. ((ge_int_bool(x, y) = true) <-> (x >= y))))
axiom eq_int_bool_axiom:
(forall x:int. (forall y:int. ((eq_int_bool(x, y) = true) <-> (x = y))))
axiom neq_int_bool_axiom:
(forall x:int. (forall y:int. ((neq_int_bool(x, y) = true) <-> (x <> y))))
logic add_real : real, real -> real
logic sub_real : real, real -> real
logic mul_real : real, real -> real
logic div_real : real, real -> real
logic pow_real : real, real -> real
logic neg_real : real -> real
logic abs_real : real -> real
logic sqrt_real : real -> real
logic real_of_int : int -> real
logic int_of_real : real -> int
logic lt_real : real, real -> prop
logic le_real : real, real -> prop
logic gt_real : real, real -> prop
logic ge_real : real, real -> prop
logic eq_real : real, real -> prop
logic neq_real : real, real -> prop
logic lt_real_bool : real, real -> bool
logic le_real_bool : real, real -> bool
logic gt_real_bool : real, real -> bool
logic ge_real_bool : real, real -> bool
logic eq_real_bool : real, real -> bool
logic neq_real_bool : real, real -> bool
axiom lt_real_bool_axiom:
(forall x:real. (forall y:real. ((lt_real_bool(x, y) = true) <-> (x < y))))
axiom le_real_bool_axiom:
(forall x:real.
(forall y:real. ((le_real_bool(x, y) = true) <-> (x <= y))))
axiom gt_real_bool_axiom:
(forall x:real. (forall y:real. ((gt_real_bool(x, y) = true) <-> (x > y))))
axiom ge_real_bool_axiom:
(forall x:real.
(forall y:real. ((ge_real_bool(x, y) = true) <-> (x >= y))))
axiom eq_real_bool_axiom:
(forall x:real. (forall y:real. ((eq_real_bool(x, y) = true) <-> (x = y))))
axiom neq_real_bool_axiom:
(forall x:real.
(forall y:real. ((neq_real_bool(x, y) = true) <-> (x <> y))))
logic int_max : int, int -> int
logic int_min : int, int -> int
logic real_max : real, real -> real
logic real_min : real, real -> real
predicate zwf_zero(a: int, b: int) = ((0 <= b) and (a < b))
type 'a farray
logic access : 'a1 farray, int -> 'a1
logic update : 'a1 farray, int, 'a1 -> 'a1 farray
axiom access_update:
(forall a:'a1 farray.
(forall i:int. (forall v:'a1. (access(update(a, i, v), i) = v))))
axiom access_update_neq:
(forall a:'a1 farray.
(forall i:int.
(forall j:int.
(forall v:'a1.
((i <> j) -> (access(update(a, i, v), j) = access(a, j)))))))
logic array_length : 'a1 farray -> int
predicate sorted_array(t: int farray, i: int, j: int) =
(forall k1:int.
(forall k2:int.
((((i <= k1) and (k1 <= k2)) and (k2 <= j)) -> (access(t,
k1) <= access(t, k2)))))
predicate exchange(a1: 'a1 farray, a2: 'a1 farray, i: int, j: int) =
((array_length(a1) = array_length(a2)) and
((access(a1, i) = access(a2, j)) and
((access(a2, i) = access(a1, j)) and
(forall k:int.
(((k <> i) and (k <> j)) -> (access(a1, k) = access(a2, k)))))))
logic permut : 'a1 farray, 'a1 farray, int, int -> prop
axiom permut_refl:
(forall t:'a1 farray. (forall l:int. (forall u:int. permut(t, t, l, u))))
axiom permut_sym:
(forall t1:'a1 farray.
(forall t2:'a1 farray.
(forall l:int.
(forall u:int. (permut(t1, t2, l, u) -> permut(t2, t1, l, u))))))
axiom permut_trans:
(forall t1:'a1 farray.
(forall t2:'a1 farray.
(forall t3:'a1 farray.
(forall l:int.
(forall u:int.
(permut(t1, t2, l, u) ->
(permut(t2, t3, l, u) -> permut(t1, t3, l, u))))))))
axiom permut_exchange:
(forall a1:'a1 farray.
(forall a2:'a1 farray.
(forall l:int.
(forall u:int.
(forall i:int.
(forall j:int.
(((l <= i) and (i <= u)) ->
(((l <= j) and (j <= u)) ->
(exchange(a1, a2, i, j) -> permut(a1, a2, l, u))))))))))
axiom exchange_upd:
(forall a:'a1 farray.
(forall i:int.
(forall j:int. exchange(a, update(update(a, i, access(a, j)), j,
access(a, i)), i, j))))
axiom permut_weakening:
(forall a1:'a1 farray.
(forall a2:'a1 farray.
(forall l1:int.
(forall r1:int.
(forall l2:int.
(forall r2:int.
((((l1 <= l2) and (l2 <= r2)) and (r2 <= r1)) ->
(permut(a1, a2, l2, r2) -> permut(a1, a2, l1, r1)))))))))
axiom permut_eq:
(forall a1:'a1 farray.
(forall a2:'a1 farray.
(forall l:int.
(forall u:int.
((l <= u) ->
(permut(a1, a2, l, u) ->
(forall i:int.
(((i < l) or (u < i)) -> (access(a2, i) = access(a1, i))))))))))
predicate permutation(a1: 'a1 farray, a2: 'a1 farray) = permut(a1, a2, 0,
(array_length(a1) - 1))
axiom array_length_update:
(forall a:'a1 farray.
(forall i:int.
(forall v:'a1. (array_length(update(a, i, v)) = array_length(a)))))
axiom permut_array_length:
(forall a1:'a1 farray.
(forall a2:'a1 farray.
(forall l:int.
(forall u:int.
(permut(a1, a2, l, u) -> (array_length(a1) = array_length(a2)))))))
logic min : int, int -> int
axiom min_ax: (forall x:int. (forall y:int. (min(x, y) <= x)))
goal f_po_1:
forall n:int.
forall r0:int.
forall r:int.
(r = min(r0, n)) ->
(r <= r0)
why-2.14-Makefile.in.patch:
--- NEW FILE why-2.14-Makefile.in.patch ---
--- Makefile.in 2008-07-28 08:03:03.000000000 -0400
+++ Makefile.in 2008-08-01 00:13:23.000000000 -0400
@@ -208,6 +208,7 @@
bin/why.opt: $(CMX) src/why.cmx
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ unix.cmxa str.cmxa nums.cmxa graph.cmxa $^
$(STRIP) $@
+ execstack -c $@
bin/why.byte: $(CMO) src/why.cmo
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLC) $(BFLAGS) -o $@ unix.cma str.cma nums.cma graph.cma $^
@@ -258,6 +259,7 @@
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLOPT) \
$(OFLAGS) -o $@ unix.cmxa str.cmxa graph.cmxa $^
$(STRIP) $@
+ execstack -c $@
bin/caduceus.byte: $(CCMA) $(CCMO)
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLC) \
@@ -315,6 +317,7 @@
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) $(APRONLIB) $(APRONLIBS) $(ATPLIB) -o $@ \
unix.cmxa nums.cmxa graph.cmxa $^
$(STRIP) $@
+ execstack -c $@
bin/jessie.byte: $(JCCMO)
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLC) $(BFLAGS) $(APRONLIB) $(APRONBYTLIBS) $(ATPLIB) -o $@ \
@@ -343,6 +346,7 @@
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ \
unix.cmxa nums.cmxa graph.cmxa $^
$(STRIP) $@
+ execstack -c $@
bin/krakatoa.byte: $(KCMO)
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLC) $(BFLAGS) -o $@ \
@@ -502,6 +506,7 @@
bin/gwhy.opt: $(GCMX)
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLOPT) $(OFLAGS) -o $@ unix.cmxa threads.cmxa nums.cmxa str.cmxa graph.cmxa lablgtk.cmxa gtkThread.cmx $^
$(STRIP) $@
+ execstack -c $@
bin/gwhy.byte: $(GCMO)
$(if $(QUIET), at echo 'Linking $@' &&) $(OCAMLC) $(BFLAGS) -o $@ unix.cma str.cma nums.cma graph.cma lablgtk.cma threads.cma gtkThread.cmo $^
@@ -518,6 +523,7 @@
bin/why2html.opt: tools/why2html.ml
$(OCAMLOPT) $(OFLAGS) -o $@ $^
+ execstack -c $@
SIMPLIFYTOWHYCMO=src/ident.cmo src/pp.cmo \
tools/simplify_parser.cmo tools/simplify_lexer.cmo \
@@ -529,6 +535,7 @@
bin/simplify2why.opt: $(SIMPLIFYTOWHYCMX)
$(OCAMLOPT) $(OFLAGS) -o $@ $^
+ execstack -c $@
DPCMO = tools/cvcl_split.cmo tools/simplify_split.cmo tools/smtlib_split.cmo\
tools/zenon_split.cmo tools/ergo_split.cmo tools/rv_split.cmo \
@@ -540,6 +547,7 @@
bin/why-dp.opt: $(DPCMX)
$(OCAMLOPT) $(OFLAGS) -o $@ unix.cmxa $^
+ execstack -c $@
bin/why-cpulimit: tools/cpulimit.c
$(CC) -o $@ $^
@@ -549,6 +557,7 @@
bin/rv_merge.opt: tools/rv_merge.ml
$(OCAMLOPT) $(OFLAGS) -o $@ $^
+ execstack -c $@
OBFCMO=src/pp.cmo src/loc.cmo src/ident.cmo src/float_lexer.cmo \
src/parser.cmo src/lexer.cmo tools/obfuscator.cmo
@@ -559,6 +568,7 @@
bin/why-obfuscator.opt: $(OBFCMX)
$(OCAMLOPT) $(OFLAGS) -o $@ $^
+ execstack -c $@
STATCMO=src/pp.cmo src/loc.cmo src/ident.cmo src/float_lexer.cmo \
src/parser.cmo src/lexer.cmo tools/whystat.cmo
@@ -569,6 +579,7 @@
bin/why-stat.opt: $(STATCMX)
$(OCAMLOPT) $(OFLAGS) -o $@ $^
+ execstack -c $@
bin/cadlog.opt: c/cversion.cmx jc/jc_version.cmx \
java/java_version.cmx tools/cadlog.cmx
@@ -737,15 +748,9 @@
cp -f $(V7FILES) $(LIBDIR)/why/coq7
cp -f $(VO7) $(LIBDIR)/why/coq7
install-coq-v8:
- if test -w $(COQLIB) ; then \
- mkdir -p $(COQLIB)/user-contrib ; \
- cp -f $(V8FILES) $(COQLIB)/user-contrib ; \
- cp -f $(VO8) $(COQLIB)/user-contrib ; \
- else \
- echo "Cannot copy to Coq standard library. Add $(LIBDIR)/why/coq to Coq include path." ;\
- mkdir -p $(LIBDIR)/why/coq ;\
- cp -f $(VO8) $(V8FILES) $(LIBDIR)/why/coq ;\
- fi
+ mkdir -p $(COQLIB)/user-contrib
+ cp -f $(V8FILES) $(COQLIB)/user-contrib
+ cp -f $(VO8) $(COQLIB)/user-contrib
install-pvs-no:
install-pvs-yes: $(PVSFILES)
why-config.patch:
--- NEW FILE why-config.patch ---
--- intf/config.mll 2008-07-28 08:03:03.000000000 -0400
+++ intf/config.mll 2008-07-31 22:52:45.000000000 -0400
@@ -47,11 +47,12 @@
let create_default_config () =
if not (Sys.file_exists config_file) then begin
let out_channel = open_out config_file in
- output_string out_channel "prover = \"Simplify\"\n";
+ output_string out_channel "prover = \"alt-ergo\"\n";
output_string out_channel "cache = \"true\"\n";
output_string out_channel "timeout = \"10\"\n";
output_string out_channel "hard_proof = \"true\"\n";
output_string out_channel "live_update = \"false\"\n";
+ output_string out_channel "provers = \"Zenon\" \"CVC3\" \"alt-ergo\"\n";
try close_out out_channel
with Sys_error s -> prerr_string s
end
--- NEW FILE why.spec ---
Name: why
Version: 2.14
Release: 2%{?dist}
Summary: Why software verification platform
Group: Applications/Engineering
License: GPLv2
URL: http://why.lri.fr/
Source0: http://why.lri.fr/download/why-2.14.tar.gz
Source1: README.why-gwhy.Fedora
Source2: README.why-coq.Fedora
Source3: README.why
Source4: gwhy.desktop
Source5: gwhy-icon.png
Source6: min.mlw
Source7: min_why.why.result
Source8: http://caduceus.lri.fr/manual/caduceus.ps
Source9: http://gforge.inria.fr/docman/view.php/999/5097/krakatoa.pdf
Patch0: gwhy-2.14.patch
Patch1: why-2.14-Makefile.in.patch
Patch2: why-config.patch
BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
BuildRequires: ocaml >= 3.09, ocaml-camlp4-devel, gtk2-devel, ocaml-lablgtk-devel, desktop-file-utils, dos2unix, prelink, coq
%description
Why is a software verification platform that applies formal proving
tools to annotated programs. It is currently capable of analysis of C
(through the included tool "Caduceus"), Java (through the included
tool "Krakatoa"), and potentially ML programs with some modification
into Why's own ML-like language. Furthermore, Why is capable of
analysis of any program that is mapped onto its own internal
language. It uses a weakest precondition involving calculus to
generate potential theorems necessary for the proof of a program's
correctness. It translates these theorems into formats that can be
used by external proof assistants (without any extra work, Coq, PVS,
HOL Light, Mizar are supported - having one is recommended and Coq is
packaged for Fedora) and automated theorem provers (without any extra
work, Simplify, Alt-Ergo, Yices, Z3, CVC Lite, Zenon are supported and
Zenon is packaged for Fedora) so that these results can be externally
proven, resulting in a proof of program correctness.
%package gwhy
Group: Applications/Engineering
Summary: IDE for Why software verification platform
Requires: why = %{version}, zenity
%description gwhy
Gwhy is an optional graphical user interface for the Why software
coordination platform. It assists in the coordination of dispatching
assertions that need to be proven to different theorem provers by
providing an interface to do this and also supports inspection of why
input files.
%package coq
Group: Applications/Engineering
Summary: Libraries for interfacing Coq with Why
Requires: why = %{version}
%description coq
This package contains a set of routines that assist in the
manipulation of why Coq-formatted output within Coq.
%prep
%setup -q
# The gwhy execution shell script is not particularly informative
# about when bad parameters are passed to it - this patch fixes that
# Upstream has been informed about this issue and a better fix is on
# their todo list, perhaps for 2.15
%patch0
# This patch makes a Fedora-specific fix to eliminate checking for the
# location of Coq - since we're using the coq package, we know where
# it is and their checking causes the rpm building to fail
%patch1
# This patch fixes the creation of a default configuration file in Why
# to use more sensible values for default provers chosen to appear in
# the lefthand GUI window
%patch2
cp %SOURCE1 %SOURCE2 %SOURCE3 %SOURCE4 %SOURCE5 %SOURCE6 %SOURCE7 %SOURCE8 %SOURCE9 .
%build
%define opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
# Native ocaml builds do not seem to work on ppc64 (many packages have
# this problem)
%ifarch ppc64
%define opt 0
%endif
# If not building opt, disable the debug info creation as this would otherwise destroy the bytecode executables
# If we have opt, as this has a dependency on ocaml, we should have ocamlopt.opt
%if ! %{opt}
%define __os_install_post /usr/lib/rpm/brp-compress %{nil}
%define _enable_debug_package 0
%define debug_package %{nil}
%define opt_option OCAMLBEST=byte OCAMLC=ocamlc OCAMLDEP=ocamldep OCAMLYACC=ocamlyacc OCAMLLEX=ocamllex
%else
%define opt_option OCAMLBEST=opt OCAMLOPT=ocamlopt.opt
%endif
# We actually want to install library files into a non /usr/lib
# directory as they aren't architecture dependent
./configure --prefix=%{_prefix} --bindir=%{_bindir} --libdir=%{_datadir} --mandir=%{_mandir}
make %{opt_option}
%check
%if %opt
%define why bin/why.opt
%else
%define why bin/why.byte
%endif
export WHYLIB=lib/why
%why --why --output min min.mlw
unset WHYLIB
diff min_why.why min_why.why.result > /dev/null
%install
rm -rf %{buildroot}
make %{opt_option} BINDIR=%{buildroot}%{_bindir} LIBDIR=%{buildroot}%{_datadir} MANDIR=%{buildroot}%{_mandir} COQLIB=%{buildroot}%{_datadir}/coq install
# Install desktop icon and menu entry
%define why_data_dir %{_datadir}/why
%if %(test -d %{buildroot}%{why_data_dir} && echo 1 || echo 0) != 1
mkdir -p %{buildroot}%{why_data_dir}
%endif
cp gwhy-icon.png %{buildroot}%{why_data_dir}
sed -i -e 's|ICON-LOCATION-BASE|%{why_data_dir}|' gwhy.desktop
desktop-file-install --vendor="fedora" \
--dir=%{buildroot}%{_datadir}/applications \
gwhy.desktop
%define why_doc_dir %{_defaultdocdir}/%{name}-%{version}/
%define why_examples_dir %{why_doc_dir}examples/
# Fix up documentation and examples
mkdir -p %{buildroot}%{why_examples_dir}mlw/
mkdir -p %{buildroot}%{why_examples_dir}c/
cp -p doc/manual.ps %{buildroot}%{why_doc_dir}why-manual.ps
cp -p caduceus.ps krakatoa.pdf README.why COPYING GPL %{buildroot}%{why_doc_dir}
# Copy in the example files after converting to proper UTF-8, fix line
# encodings, leaving behind all generated files
cd examples
for d in `find -mindepth 1 -maxdepth 1 -type d`; do
mkdir -p %{buildroot}%{why_examples_dir}mlw/$d
done
for f in `find -regex '.*\(\.mlw\|\.why\)' | egrep -v '_inv|_coq|_why'`; do
dos2unix $f; mv $f $f.old; iconv -f ISO-8859-1 -t UTF-8 < $f.old > $f; rm $f.old
cp -p $f %{buildroot}%{why_examples_dir}mlw/$f
done
cd ../examples-c
for d in `find -mindepth 1 -maxdepth 1 -type d`; do
mkdir -p %{buildroot}%{why_examples_dir}c/$d
done
for f in `find -regex '.*\.c'`; do
dos2unix $f; mv $f $f.old; iconv -f ISO-8859-1 -t UTF-8 < $f.old > $f; rm $f.old
cp -p $f %{buildroot}%{why_examples_dir}c/$f
done
%clean
rm -rf %{buildroot}
%files
%defattr(-,root,root,-)
# Binaries
%{_bindir}/*
%exclude %{_bindir}/gwhy*
# Data for programs
%{_datadir}/why
%{_datadir}/caduceus
%{_datadir}/jessie
%{_datadir}/krakatoa
%exclude %{_datadir}/jessie/jc.cmo
%if %opt
%exclude %{_datadir}/jessie/jc.cmx
%endif
# Man page
%{_mandir}/man1/why.1.gz
# Documentation and examples
%{why_doc_dir}
# This last example is really an example only for Coq - only .v files
%exclude %{why_examples_dir}mlw/string-matching/
%files gwhy
%defattr(-,root,root,-)
%{_bindir}/gwhy
%{_bindir}/gwhy-bin
%dir %{why_data_dir}
%doc README.why-gwhy.Fedora
%{why_data_dir}/gwhy-icon.png
%{_datadir}/applications/fedora-gwhy.desktop
%files coq
%defattr(-,root,root,-)
%{_datadir}/coq/user-contrib/Why*
%exclude %{_datadir}/coq/user-contrib/Why*.v
%{_datadir}/coq/user-contrib/caduceus*
%exclude %{_datadir}/coq/user-contrib/caduceus*.v
%{_datadir}/coq/user-contrib/Caduceus.v*
%exclude %{_datadir}/coq/user-contrib/Caduceus.v
%{_datadir}/coq/user-contrib/jessie_why.v*
%exclude %{_datadir}/coq/user-contrib/jessie_why.v
%doc README.why-coq.Fedora
%changelog
* Fri Aug 1 2008 Alan Dunn <amdunn at gmail.com> 2.14-2
- Fixed minor issues in response to package review:
- Inclusion of COPYING, GPL license-related files
- Added config.mll patch to make default config file created nicer
- Changes subpackage dependencies to be fully versioned.
- Makes during build allowed to be noisy (allowed to print).
* Wed Jul 30 2008 Alan Dunn <amdunn at gmail.com> 2.14-1
- Changed to new version of why, removed previous why-cpulimit name
change, zenon output format patches as the issues were fixed in
why 2.14.
- Moved doc subpackage back into main package.
- Added example files to documentation subpackage.
- Added check section with test on small why file.
- Reformatted some macro names for greater readability.
* Thu Jul 24 2008 Alan Dunn <amdunn at gmail.com> 2.13-2
- Added several patches: fixed Zenon output, completed fix of rename
of cpulimit -> why-cpulimit.
* Wed Jul 23 2008 Alan Dunn <amdunn at gmail.com> 2.13-1
- Initial Fedora RPM version.
Index: .cvsignore
===================================================================
RCS file: /cvs/pkgs/rpms/why/devel/.cvsignore,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -r1.1 -r1.2
--- .cvsignore 4 Aug 2008 18:32:10 -0000 1.1
+++ .cvsignore 5 Aug 2008 16:49:17 -0000 1.2
@@ -0,0 +1,2 @@
+krakatoa.pdf
+why-2.14.tar.gz
Index: sources
===================================================================
RCS file: /cvs/pkgs/rpms/why/devel/sources,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -r1.1 -r1.2
--- sources 4 Aug 2008 18:32:10 -0000 1.1
+++ sources 5 Aug 2008 16:49:17 -0000 1.2
@@ -0,0 +1,2 @@
+56c2e53b7ef4dae8afe4e8264ac44419 krakatoa.pdf
+d88c0577f2af4ae73631f42e2695cac0 why-2.14.tar.gz
- Previous message (by thread): rpms/gnome-panel/devel .cvsignore, 1.80, 1.81 gnome-panel.spec, 1.311, 1.312 preferred-apps.patch, 1.7, 1.8 sources, 1.83, 1.84 gnome-panel-2.13.5-switch-user.patch, 1.3, NONE gnome-panel-2.19.5-vendor.patch, 1.1, NONE gnome-panel-2.22.0-ck-shutdown.patch, 1.3, NONE gnome-panel-larger-find-window.patch, 1.1, NONE gnome-panel-launch-with-gio.patch, 1.3, NONE gnome-panel-use-gio.patch, 1.1, NONE icon-names.patch, 1.2, NONE timezone-debug.patch, 1.2, NONE
- Next message (by thread): rpms/orca/devel .cvsignore, 1.35, 1.36 orca.spec, 1.57, 1.58 sources, 1.36, 1.37
- Messages sorted by:
[ date ]
[ thread ]
[ subject ]
[ author ]
More information about the fedora-extras-commits
mailing list