Spaces:
Sleeping
Sleeping
LHospital13
commited on
Commit
•
1c06f52
1
Parent(s):
3715d21
Implemented password logic
Browse files
README.md
CHANGED
@@ -10,7 +10,7 @@ pinned: false
|
|
10 |
license: unknown
|
11 |
---
|
12 |
|
13 |
-
#
|
14 |
|
15 |
感谢您在百忙之中抽出时间帮助我们完成课题!在本次调研中,您需要对约30个带形式语言规约的Java程序进行打分,以评估这些规约的语义是否足够有效且用户友好。调研总共需耗时约20分钟。
|
16 |
|
@@ -43,12 +43,12 @@ public class IsAscending {
|
|
43 |
|
44 |
```
|
45 |
|
46 |
-
|
47 |
|
48 |
+ `requires`语句描述某方法的参数应当满足的条件;
|
49 |
+ `ensures`语句描述某方法在满足`requires`语句所描述的条件时,其返回值`\result`与各个参数应当满足的关系;
|
50 |
+ `maintaining`语句描述`while`、`for`等语句应当满足的循环不变式。由该语句所描述的规约应当在进入循环时、每次循环体执行前以及(因循环条件不满足)退出循环时均成立;
|
51 |
-
+ `decreases
|
52 |
+ `assume`语句用于辅助JML验证器对JML的正确性进行验证,其含义是显式告诉验证器,相应的布尔表达式在该程序点必然为真。
|
53 |
|
54 |
大多数JML语句中都会包含一个表达式。表达式的形式与Java中常见的表达式基本一致,但为了充分表达程序可能满足的性质,JML对表达式中能够出现的谓词与操作符都进行了一定扩展,包括表示蕴含的逻辑操作符`==>`、`<==`以及`<==>`、与$\forall$与$\exists$相对应的谓词`\forall`与`\exists`等。例如,表达式`\result == true <==> (\forall int i; 0 <= i && i < arr.length-1; arr[i] < arr[i+1])`的含义为:方法返回值为真,当且仅当对于从`0`到`arr.length-2`的每个整数`i`,都有`arr[i] < arr[i+1]`。
|
@@ -114,4 +114,4 @@ public class IsAscending {
|
|
114 |
|
115 |
|
116 |
|
117 |
-
##
|
|
|
10 |
license: unknown
|
11 |
---
|
12 |
|
13 |
+
# 程序规约有效性评估——用户调研
|
14 |
|
15 |
感谢您在百忙之中抽出时间帮助我们完成课题!在本次调研中,您需要对约30个带形式语言规约的Java程序进行打分,以评估这些规约的语义是否足够有效且用户友好。调研总共需耗时约20分钟。
|
16 |
|
|
|
43 |
|
44 |
```
|
45 |
|
46 |
+
拥有超强代码能力的您不难看出,该程序可以判断整型数组`arr`是否是单调递增的。该程序中的注释即为描述程序行为的JML,每个JML语句占据一行单行注释,以分号作为结尾。在该样例中:
|
47 |
|
48 |
+ `requires`语句描述某方法的参数应当满足的条件;
|
49 |
+ `ensures`语句描述某方法在满足`requires`语句所描述的条件时,其返回值`\result`与各个参数应当满足的关系;
|
50 |
+ `maintaining`语句描述`while`、`for`等语句应当满足的循环不变式。由该语句所描述的规约应当在进入循环时、每次循环体执行前以及(因循环条件不满足)退出循环时均成立;
|
51 |
+
+ `decreases`语句是一种细分的循环不变式,其含义是表达式的取值在每次循环后都会变小;
|
52 |
+ `assume`语句用于辅助JML验证器对JML的正确性进行验证,其含义是显式告诉验证器,相应的布尔表达式在该程序点必然为真。
|
53 |
|
54 |
大多数JML语句中都会包含一个表达式。表达式的形式与Java中常见的表达式基本一致,但为了充分表达程序可能满足的性质,JML对表达式中能够出现的谓词与操作符都进行了一定扩展,包括表示蕴含的逻辑操作符`==>`、`<==`以及`<==>`、与$\forall$与$\exists$相对应的谓词`\forall`与`\exists`等。例如,表达式`\result == true <==> (\forall int i; 0 <= i && i < arr.length-1; arr[i] < arr[i+1])`的含义为:方法返回值为真,当且仅当对于从`0`到`arr.length-2`的每个整数`i`,都有`arr[i] < arr[i+1]`。
|
|
|
114 |
|
115 |
|
116 |
|
117 |
+
## 再次感谢您对本课题做出的贡献!
|
app.py
CHANGED
@@ -3,6 +3,7 @@ from __future__ import annotations
|
|
3 |
import json
|
4 |
import logging
|
5 |
import random
|
|
|
6 |
from functools import partial
|
7 |
from pathlib import Path
|
8 |
|
@@ -13,6 +14,7 @@ logger.setLevel(logging.DEBUG)
|
|
13 |
logging.basicConfig(format="%(asctime)s [%(levelname)s] - %(message)s")
|
14 |
|
15 |
dump_score = "scores.json"
|
|
|
16 |
|
17 |
# load code samples
|
18 |
# samples_num = 0
|
@@ -30,9 +32,13 @@ logger.info(f"Loaded {len(samples)} samples")
|
|
30 |
|
31 |
# map from user name to {file name: score}
|
32 |
global_score: dict[str, dict[str, int]] = dict()
|
|
|
33 |
if Path(dump_score).exists():
|
34 |
with open(dump_score, encoding="utf-8") as f:
|
35 |
global_score = json.load(f)
|
|
|
|
|
|
|
36 |
|
37 |
score_desc = [
|
38 |
"",
|
@@ -40,7 +46,7 @@ score_desc = [
|
|
40 |
"有规约,但其意义过于trivial,对于任何类似pattern的代码都有效",
|
41 |
"规约有一定意义,但对于理解程序实际所做的事没有什么帮助",
|
42 |
"规约能够充分描述程序中某些部分应满足的性质,但尚不足以完全描述整个程序所做的事",
|
43 |
-
"
|
44 |
]
|
45 |
help_markdown = Path("README.md").read_text(encoding="utf-8")
|
46 |
|
@@ -50,7 +56,7 @@ with gr.Blocks(title="程序规约有效性评估——用户调研") as demo:
|
|
50 |
selected_index = gr.State([])
|
51 |
def select_index(selected_index):
|
52 |
array = [0]
|
53 |
-
array.extend(random.sample(range(1, samples_num), selected_num))
|
54 |
array.sort()
|
55 |
return array
|
56 |
demo.load(select_index, inputs=[selected_index], outputs=[selected_index])
|
@@ -61,7 +67,7 @@ with gr.Blocks(title="程序规约有效性评估——用户调研") as demo:
|
|
61 |
title = gr.HTML("<h1><center>程序规约有效性评估——请先展开README</center></h1>")
|
62 |
with gr.Accordion(label="Readme", open=False):
|
63 |
help = gr.Markdown(help_markdown)
|
64 |
-
with gr.Accordion(label="Info", open=True) as info_accordion:
|
65 |
user_name = gr.Textbox(label="Nickname",
|
66 |
placeholder="Enter your nickname, anything would be fine",
|
67 |
interactive=True,
|
@@ -69,6 +75,8 @@ with gr.Blocks(title="程序规约有效性评估——用户调研") as demo:
|
|
69 |
)
|
70 |
user_gender = gr.Radio(
|
71 |
["Male", "Female", "Other", "Prefer Undisclosed"],
|
|
|
|
|
72 |
label="Gender"
|
73 |
)
|
74 |
user_age = gr.Textbox(label="Age",
|
@@ -78,7 +86,8 @@ with gr.Blocks(title="程序规约有效性评估——用户调研") as demo:
|
|
78 |
)
|
79 |
user_major = gr.Dropdown(
|
80 |
label="Major",
|
81 |
-
choices=["Architecture", "Astronomy", "Biology", "Chemistry", "Computer Science", "Earth Science", "Electrical Science", "Environmental Science", "Materials Science", "Mathematics", "Physics", "Others"],
|
|
|
82 |
multiselect=False,
|
83 |
interactive=True
|
84 |
)
|
@@ -101,11 +110,11 @@ with gr.Blocks(title="程序规约有效性评估——用户调研") as demo:
|
|
101 |
value=score_desc[value], label="Description"),
|
102 |
inputs=[score_slider],
|
103 |
outputs=[score_description])
|
104 |
-
submit = gr.Button(value="Submit", variant="primary")
|
105 |
|
106 |
with gr.Row():
|
107 |
code_title = gr.HTML(
|
108 |
-
f"<h2>{
|
109 |
# code_select = gr.Dropdown(
|
110 |
# choices=file_names_with_id,
|
111 |
# value=file_names_with_id[index.value],
|
@@ -119,13 +128,26 @@ with gr.Blocks(title="程序规约有效性评估——用户调研") as demo:
|
|
119 |
samples[index.value],
|
120 |
language="javascript",
|
121 |
)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
122 |
|
123 |
button_next = gr.Button(value=">")
|
124 |
|
125 |
-
def update_index(file_index: int, selected_index:
|
126 |
-
|
127 |
for i, index in enumerate(selected_index):
|
128 |
if index == file_index:
|
|
|
129 |
file_index = selected_index[(i + delta) % len(selected_index)]
|
130 |
break
|
131 |
# file_index = (file_index + delta + len(samples)) % len(samples)
|
@@ -134,7 +156,13 @@ with gr.Blocks(title="程序规约有效性评估——用户调研") as demo:
|
|
134 |
scores = global_score.get(username, dict())
|
135 |
# set score if exists
|
136 |
if file_name not in scores:
|
137 |
-
slider =
|
|
|
|
|
|
|
|
|
|
|
|
|
138 |
desc = score_desc[1]
|
139 |
else:
|
140 |
slider = gr.Slider(
|
@@ -145,11 +173,11 @@ with gr.Blocks(title="程序规约有效性评估——用户调研") as demo:
|
|
145 |
label="Score",
|
146 |
)
|
147 |
desc = score_desc[scores[file_name]]
|
148 |
-
return (file_index, f"<h2>{
|
149 |
samples[file_index], slider, desc, file_name_id)
|
150 |
|
151 |
-
def submit_score(file_index: int,
|
152 |
-
username: str,
|
153 |
value: int,
|
154 |
notify_name: bool = True):
|
155 |
# first check if user name is set
|
@@ -162,6 +190,7 @@ with gr.Blocks(title="程序规约有效性评估——用户调研") as demo:
|
|
162 |
|
163 |
filename = file_names[file_index]
|
164 |
scores = global_score.setdefault(username, dict())
|
|
|
165 |
|
166 |
# check if user name duplicated
|
167 |
if notify_name and filename in scores:
|
@@ -173,11 +202,12 @@ with gr.Blocks(title="程序规约有效性评估——用户调研") as demo:
|
|
173 |
num_scored_prev = len(scores)
|
174 |
# update the score to global score
|
175 |
global_score[username][filename] = value
|
|
|
176 |
# check if all files scored
|
177 |
num_scored = len(global_score[username])
|
178 |
-
if num_scored ==
|
179 |
gr.Info(
|
180 |
-
"Congratulations! All
|
181 |
logging.info(f"User {username} scored all files.")
|
182 |
|
183 |
# get all scores of i
|
@@ -195,6 +225,9 @@ with gr.Blocks(title="程序规约有效性评估——用户调研") as demo:
|
|
195 |
# dump global score
|
196 |
with open(dump_score, "w", encoding="utf-8") as f:
|
197 |
json.dump(global_score, f, ensure_ascii=False, indent=4)
|
|
|
|
|
|
|
198 |
|
199 |
# update index by 1
|
200 |
return *update_index(file_index, selected_index, username, delta=1), notify_name
|
@@ -202,6 +235,18 @@ with gr.Blocks(title="程序规约有效性评估——用户调研") as demo:
|
|
202 |
def select_code(filename_id: str, username: str):
|
203 |
file_index = file_names_with_id.index(filename_id)
|
204 |
return update_index(file_index, selected_index, username, delta=0)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
205 |
|
206 |
inputs = [index, selected_index, user_name]
|
207 |
outputs = [
|
@@ -212,7 +257,9 @@ with gr.Blocks(title="程序规约有效性评估——用户调研") as demo:
|
|
212 |
button_prev.click(partial(update_index, delta=-1), inputs, outputs)
|
213 |
button_next.click(partial(update_index, delta=+1), inputs, outputs)
|
214 |
submit.click(submit_score,
|
215 |
-
inputs=[index,
|
|
|
|
|
216 |
outputs=[
|
217 |
index, code_title, code_block, score_slider,
|
218 |
score_description, code_select, notify_same_name
|
@@ -222,5 +269,7 @@ with gr.Blocks(title="程序规约有效性评估——用户调研") as demo:
|
|
222 |
# inputs=[code_select, user_name],
|
223 |
# outputs=outputs)
|
224 |
|
|
|
|
|
225 |
if __name__ == "__main__":
|
226 |
demo.queue().launch(debug=True, share=False)
|
|
|
3 |
import json
|
4 |
import logging
|
5 |
import random
|
6 |
+
import hashlib
|
7 |
from functools import partial
|
8 |
from pathlib import Path
|
9 |
|
|
|
14 |
logging.basicConfig(format="%(asctime)s [%(levelname)s] - %(message)s")
|
15 |
|
16 |
dump_score = "scores.json"
|
17 |
+
dump_info = "userinfo.json"
|
18 |
|
19 |
# load code samples
|
20 |
# samples_num = 0
|
|
|
32 |
|
33 |
# map from user name to {file name: score}
|
34 |
global_score: dict[str, dict[str, int]] = dict()
|
35 |
+
global_info: dict[str, list[str, str, str]] = dict()
|
36 |
if Path(dump_score).exists():
|
37 |
with open(dump_score, encoding="utf-8") as f:
|
38 |
global_score = json.load(f)
|
39 |
+
if Path(dump_info).exists():
|
40 |
+
with open(dump_info, encoding="utf-8") as f:
|
41 |
+
global_info = json.load(f)
|
42 |
|
43 |
score_desc = [
|
44 |
"",
|
|
|
46 |
"有规约,但其意义过于trivial,对于任何类似pattern的代码都有效",
|
47 |
"规约有一定意义,但对于理解程序实际所做的事没有什么帮助",
|
48 |
"规约能够充分描述程序中某些部分应满足的性质,但尚不足以完全描述整个程序所做的事",
|
49 |
+
"规约能够充分描述程序整体与各个部分的行为",
|
50 |
]
|
51 |
help_markdown = Path("README.md").read_text(encoding="utf-8")
|
52 |
|
|
|
56 |
selected_index = gr.State([])
|
57 |
def select_index(selected_index):
|
58 |
array = [0]
|
59 |
+
array.extend(random.sample(range(1, samples_num), selected_num - 1))
|
60 |
array.sort()
|
61 |
return array
|
62 |
demo.load(select_index, inputs=[selected_index], outputs=[selected_index])
|
|
|
67 |
title = gr.HTML("<h1><center>程序规约有效性评估——请先展开README</center></h1>")
|
68 |
with gr.Accordion(label="Readme", open=False):
|
69 |
help = gr.Markdown(help_markdown)
|
70 |
+
with gr.Accordion(label="User Info", open=True) as info_accordion:
|
71 |
user_name = gr.Textbox(label="Nickname",
|
72 |
placeholder="Enter your nickname, anything would be fine",
|
73 |
interactive=True,
|
|
|
75 |
)
|
76 |
user_gender = gr.Radio(
|
77 |
["Male", "Female", "Other", "Prefer Undisclosed"],
|
78 |
+
value="Unknown",
|
79 |
+
interactive=True,
|
80 |
label="Gender"
|
81 |
)
|
82 |
user_age = gr.Textbox(label="Age",
|
|
|
86 |
)
|
87 |
user_major = gr.Dropdown(
|
88 |
label="Major",
|
89 |
+
choices=["Architecture", "Astronomy", "Biology", "Chemistry", "Computer Science", "Earth Science", "Economics and Finance", "Electrical Science", "Environmental Science", "Materials Science", "Mathematics", "Physics", "Others"],
|
90 |
+
value="Unknown",
|
91 |
multiselect=False,
|
92 |
interactive=True
|
93 |
)
|
|
|
110 |
value=score_desc[value], label="Description"),
|
111 |
inputs=[score_slider],
|
112 |
outputs=[score_description])
|
113 |
+
submit = gr.Button(value="Submit this quesion", variant="primary")
|
114 |
|
115 |
with gr.Row():
|
116 |
code_title = gr.HTML(
|
117 |
+
f"<h2>(01/{selected_num:02d}) {file_names[index.value]}</h2>")
|
118 |
# code_select = gr.Dropdown(
|
119 |
# choices=file_names_with_id,
|
120 |
# value=file_names_with_id[index.value],
|
|
|
128 |
samples[index.value],
|
129 |
language="javascript",
|
130 |
)
|
131 |
+
|
132 |
+
pswd_box = gr.Textbox(interactive=True)
|
133 |
+
|
134 |
+
with gr.Row():
|
135 |
+
res_block1 = gr.Code(
|
136 |
+
language="javascript",
|
137 |
+
visible=False
|
138 |
+
)
|
139 |
+
res_block2 = gr.Code(
|
140 |
+
language="javascript",
|
141 |
+
visible=False
|
142 |
+
)
|
143 |
|
144 |
button_next = gr.Button(value=">")
|
145 |
|
146 |
+
def update_index(file_index: int, selected_index: list, username: str, delta: int):
|
147 |
+
progress = 0
|
148 |
for i, index in enumerate(selected_index):
|
149 |
if index == file_index:
|
150 |
+
progress = (i + delta) % len(selected_index) + 1
|
151 |
file_index = selected_index[(i + delta) % len(selected_index)]
|
152 |
break
|
153 |
# file_index = (file_index + delta + len(samples)) % len(samples)
|
|
|
156 |
scores = global_score.get(username, dict())
|
157 |
# set score if exists
|
158 |
if file_name not in scores:
|
159 |
+
slider = gr.Slider(
|
160 |
+
minimum=1,
|
161 |
+
maximum=5,
|
162 |
+
step=1,
|
163 |
+
value=1,
|
164 |
+
label="Score",
|
165 |
+
)
|
166 |
desc = score_desc[1]
|
167 |
else:
|
168 |
slider = gr.Slider(
|
|
|
173 |
label="Score",
|
174 |
)
|
175 |
desc = score_desc[scores[file_name]]
|
176 |
+
return (file_index, f"<h2>({progress:02d}/{len(selected_index):02d}) {file_name}</h2>",
|
177 |
samples[file_index], slider, desc, file_name_id)
|
178 |
|
179 |
+
def submit_score(file_index: int, selected_index: list,
|
180 |
+
username: str, usergender:str, userage:str, usermajor:str,
|
181 |
value: int,
|
182 |
notify_name: bool = True):
|
183 |
# first check if user name is set
|
|
|
190 |
|
191 |
filename = file_names[file_index]
|
192 |
scores = global_score.setdefault(username, dict())
|
193 |
+
userinfo = global_info.setdefault(username, ["Unknown", "Unknown", "Unknown"])
|
194 |
|
195 |
# check if user name duplicated
|
196 |
if notify_name and filename in scores:
|
|
|
202 |
num_scored_prev = len(scores)
|
203 |
# update the score to global score
|
204 |
global_score[username][filename] = value
|
205 |
+
global_info[username] = [usergender, userage, usermajor]
|
206 |
# check if all files scored
|
207 |
num_scored = len(global_score[username])
|
208 |
+
if num_scored == selected_num and num_scored_prev < selected_num:
|
209 |
gr.Info(
|
210 |
+
"Congratulations! All tasks done! Thank you for your contributions!")
|
211 |
logging.info(f"User {username} scored all files.")
|
212 |
|
213 |
# get all scores of i
|
|
|
225 |
# dump global score
|
226 |
with open(dump_score, "w", encoding="utf-8") as f:
|
227 |
json.dump(global_score, f, ensure_ascii=False, indent=4)
|
228 |
+
# dump global info
|
229 |
+
with open(dump_info, "w", encoding="utf-8") as f:
|
230 |
+
json.dump(global_info, f, ensure_ascii=False, indent=4)
|
231 |
|
232 |
# update index by 1
|
233 |
return *update_index(file_index, selected_index, username, delta=1), notify_name
|
|
|
235 |
def select_code(filename_id: str, username: str):
|
236 |
file_index = file_names_with_id.index(filename_id)
|
237 |
return update_index(file_index, selected_index, username, delta=0)
|
238 |
+
|
239 |
+
def process_pswd(pswd:str):
|
240 |
+
m = hashlib.md5()
|
241 |
+
m.update(pswd.encode("utf-8"))
|
242 |
+
if m.hexdigest() == "1dde58fa912bb474be7e9bea10cdb6a0":
|
243 |
+
return (gr.Code(language="javascript",visible=True), gr.Code(language="javascript",visible=True))
|
244 |
+
return (gr.Code(language="javascript",visible=False), gr.Code(language="javascript",visible=False))
|
245 |
+
|
246 |
+
def load_result():
|
247 |
+
res1 = json.dumps(global_score, ensure_ascii=False, indent=4)
|
248 |
+
res2 = json.dumps(global_info, ensure_ascii=False, indent=4)
|
249 |
+
return (res1, res2)
|
250 |
|
251 |
inputs = [index, selected_index, user_name]
|
252 |
outputs = [
|
|
|
257 |
button_prev.click(partial(update_index, delta=-1), inputs, outputs)
|
258 |
button_next.click(partial(update_index, delta=+1), inputs, outputs)
|
259 |
submit.click(submit_score,
|
260 |
+
inputs=[index, selected_index,
|
261 |
+
user_name, user_gender, user_age, user_major,
|
262 |
+
score_slider, notify_same_name],
|
263 |
outputs=[
|
264 |
index, code_title, code_block, score_slider,
|
265 |
score_description, code_select, notify_same_name
|
|
|
269 |
# inputs=[code_select, user_name],
|
270 |
# outputs=outputs)
|
271 |
|
272 |
+
pswd_box.submit(process_pswd, inputs=[pswd_box], outputs=[res_block1, res_block2]).then(load_result, inputs=None, outputs=[res_block1, res_block2])
|
273 |
+
|
274 |
if __name__ == "__main__":
|
275 |
demo.queue().launch(debug=True, share=False)
|