里斯本的肖像

费尔南多·佩索阿在里斯本的天空上写着:“我们活过的刹那,前后皆是暗夜。”暗夜是永久的,可以大到无限,可以小到没有,星辰是久远之前的星辰。出门之后,我在寓所门外,伫立,觉得自己的生活一塌糊涂,当下即是糟糕,任何酒任何烟任何景色任何香吻都无法弥补莫名其妙的空缺,暑天长长的日头令人眩晕,没有角落会暗孕出一片风,没有人会在深夜过后的清晨说想你,大抵是繁忙,充斥在时间和往来肉体的每条缝。柳条,也不懂得勾引我了,是到中年了吧。又觉自己的生活无比丰美,当下即是未来,拔出傲剑,就有一道光,迈开腿,天就禁不住垂泪,任由冰雨在脸上无情得拍。外甥女无意间对我说,黑夜是最长的影子。才知晓孩子永远是最上等的诗人。

Read More

LeetCode - 38

Problem description

Read More

LeetCode - 39

Problem description

Read More

二〇一八七月辑

我拼命得收集大雨后的湿气味
跟我的想象力放在一块
其实已经失去你
像是我不知如何开始这一天
太阳马上又要出现了

Read More

二〇一八十一月辑

优秀的电影和文学作品,看完之后总是让人思绪万千,但同时,又从来找不到任何合适的方式表达积蓄的情感。我已经越来越不想去影院看电影了,男人快乐的方式其实也没有那么多,如今又少了一样。黑暗的环境,温暖的座椅,边上陌生女孩十分淡雅的香气,脑子里没有多余的细胞去思索她的性情编织她背后的荒原,总之,不到五分钟就在座椅上就颠了,睡死了,头就像一个延迟的不倒翁或者摆钟,一会倒在左边,一会倒在右边,加上轰鸣的音效,反而是一种类似白噪音的效果,睡半小时,仿佛睡了一整晚,模糊的意识中,冒出一些字:

Read More

蓝眼睛与红眼睛(The blue-eyed islanders puzzle)

Read More

CBMC教程 (1) - 软件架构

Read More

CBMC教程 (2) - unwind loop

Read More

CBMC教程 (3) - GOTO programs

Diffblue 团队在 CAV'18 发表了工具文章,JBMC。这个工具是 CBMC 的扩展,目的是验证 JAVA Bytecode。JBMC 的步骤和 CBMC 类似,也是前端处理程序,转换程序到公式,然后公式传递给求解器。

JBMC 的验证步骤:

Read More

CBMC (教程) - 简介

Read More