首页
网站开发
桌面应用
管理软件
微信开发
App开发
嵌入式软件
工具软件
数据采集与分析
其他
首页
>
> 详细
代做CMPT 477、Java/Python程序代写
项目预算:
开发周期:
发布时间:
要求地区:
CMPT 477/777 Formal Verification
Programming Assignment 3
This assignment is due by 11:59pm PT on Friday Nov 15, 2024. Please submit it to Canvas.
Late policy:
Suppose you can get n (out of 100) points based on your code and report
• If you submit before the deadline, you can get all n points.
• If you submit between 11:59pm PT Nov 15 and 11:59pm PT Nov 16, you get n − 10 points.
• If you submit between 11:59pm PT Nov 16 and 11:59pm PT Nov 17, you get n − 20 points.
• If you submit after 11:59pm PT Nov 17, you get 0 points.
1. (20 points) Verify the program in Algorithm 1. Note that you cannot change the existing implementation.
Algorithm 1 Find an element in the array
method Find(a : array⟨int⟩, v : int) returns (index : int)
ensures index ≥ 0 → index < a.Length ∧ a[index] = v
ensures index < 0 → ∀k. 0 ≤ k < a.Length → a[k] = v
1: var i : int := 0;
2: while i < a.Length do
3: if a[i] = v then
4: return i;
5: i := i + 1;
6: return −1;
2. (20 points) Verify the program in Algorithm 2. Note that you cannot change the existing implementation.
Algorithm 2 Sum of 10n + 10(n − 1) + . . . + 10
method Sum(n : int) returns (sum : int)
requires n > 0
ensures sum = 5n × (n + 1)
1: sum := 0;
2: var i : int := n;
3: while i > 0 do
4: var k : int := 0;
5: var j : int := i;
6: while j > 0 do
7: k := k + 10;
8: j := j − 1;
9: sum := sum + k;
10: i := i − 1;
1
3. (30 points) Given a non-empty array of integers, write a method called ArrayMin that finds the minimum
value min in the array. Verify the method can ensure
• min is less than or equal to all elements in the array
• min is equal to some element in the array
4. (30 points) Given an array of coins showing either Front or Back side on top, write a program with a
SortCoins method that sorts the coins. Verify it can ensure
• All coins showing the Front side occur before those showing Back
• The sorted array is a permutation of the original array
Deliverable
A zip file called P3 SFUID.zip that contains at least the followings:
• A file called P3 SFUID.dfy that contains Dafny programs for the above four questions.
• A report called P3 SFUID.pdf that explains the design choices, features, issues (if any), and anything
else that you want to explain about your programs.
2
软件开发、广告设计客服
QQ:99515681
邮箱:99515681@qq.com
工作时间:8:00-23:00
微信:codinghelp
热点项目
更多
代做 program、代写 c++设计程...
2024-12-23
comp2012j 代写、代做 java 设...
2024-12-23
代做 data 编程、代写 python/...
2024-12-23
代做en.553.413-613 applied s...
2024-12-23
代做steady-state analvsis代做...
2024-12-23
代写photo essay of a deciduo...
2024-12-23
代写gpa analyzer调试c/c++语言
2024-12-23
代做comp 330 (fall 2024): as...
2024-12-23
代写pstat 160a fall 2024 - a...
2024-12-23
代做pstat 160a: stochastic p...
2024-12-23
代做7ssgn110 environmental d...
2024-12-23
代做compsci 4039 programming...
2024-12-23
代做lab exercise 8: dictiona...
2024-12-23
热点标签
mktg2509
csci 2600
38170
lng302
csse3010
phas3226
77938
arch1162
engn4536/engn6536
acx5903
comp151101
phl245
cse12
comp9312
stat3016/6016
phas0038
comp2140
6qqmb312
xjco3011
rest0005
ematm0051
5qqmn219
lubs5062m
eee8155
cege0100
eap033
artd1109
mat246
etc3430
ecmm462
mis102
inft6800
ddes9903
comp6521
comp9517
comp3331/9331
comp4337
comp6008
comp9414
bu.231.790.81
man00150m
csb352h
math1041
eengm4100
isys1002
08
6057cem
mktg3504
mthm036
mtrx1701
mth3241
eeee3086
cmp-7038b
cmp-7000a
ints4010
econ2151
infs5710
fins5516
fin3309
fins5510
gsoe9340
math2007
math2036
soee5010
mark3088
infs3605
elec9714
comp2271
ma214
comp2211
infs3604
600426
sit254
acct3091
bbt405
msin0116
com107/com113
mark5826
sit120
comp9021
eco2101
eeen40700
cs253
ece3114
ecmm447
chns3000
math377
itd102
comp9444
comp(2041|9044)
econ0060
econ7230
mgt001371
ecs-323
cs6250
mgdi60012
mdia2012
comm221001
comm5000
ma1008
engl642
econ241
com333
math367
mis201
nbs-7041x
meek16104
econ2003
comm1190
mbas902
comp-1027
dpst1091
comp7315
eppd1033
m06
ee3025
msci231
bb113/bbs1063
fc709
comp3425
comp9417
econ42915
cb9101
math1102e
chme0017
fc307
mkt60104
5522usst
litr1-uc6201.200
ee1102
cosc2803
math39512
omp9727
int2067/int5051
bsb151
mgt253
fc021
babs2202
mis2002s
phya21
18-213
cege0012
mdia1002
math38032
mech5125
07
cisc102
mgx3110
cs240
11175
fin3020s
eco3420
ictten622
comp9727
cpt111
de114102d
mgm320h5s
bafi1019
math21112
efim20036
mn-3503
fins5568
110.807
bcpm000028
info6030
bma0092
bcpm0054
math20212
ce335
cs365
cenv6141
ftec5580
math2010
ec3450
comm1170
ecmt1010
csci-ua.0480-003
econ12-200
ib3960
ectb60h3f
cs247—assignment
tk3163
ics3u
ib3j80
comp20008
comp9334
eppd1063
acct2343
cct109
isys1055/3412
math350-real
math2014
eec180
stat141b
econ2101
msinm014/msing014/msing014b
fit2004
comp643
bu1002
cm2030
联系我们
- QQ: 9951568
© 2021
www.rj363.com
软件定制开发网!