LennaHammer

#lang racket
(define *sym* 0)
(define (gensym)
  (set! *sym* (+ *sym* 1))
  (string->symbol (string-append "V" (number->string *sym*) "*")))
(define (not-impl)
  (error "not-impl."))
(define (eval-argv argv nodes cont)
  (if (pair? nodes)
      (eval (car nodes)

LennaHammer

Alice’s Adventures in Wonderland, by Lewis Carroll

CHAPTER I. Down the Rabbit-Hole Alice was beginning to get very tired of sitting by her sister on the bank, and of having nothing to do: once or twice she had peeped into the book her sister was reading, but it had no pictures or conversations in it, “and what is the use of a book,” thought Alice “without pictures or conversations?”

1. Alice
2. in /in/ prep. 在...期间, 在...之内, 处于...之中, 从事于, 按照, 穿着 adv. 进入, 朝里, 在里面, 在屋里 a. 在里面的, 在朝的 n. 执政者, 交情
3. Wonderland /'wʌndәlænd/ n. 奇境, 仙境, 非常奇妙的地方

LennaHammer

必备词组

（一）由 be 构成的词组

• at 在: be good at 善于，擅长, be surprised at对...感到惊讶

• in: be interested in 对...感兴趣

• with 和: be pleased with 对...感到高兴（满意）, be satisfied with 对...感到满意, be angry with sb.生（某人的）, be covered with 被...覆盖

LennaHammer

# 参考资料
# - https://en.m.wikibooks.org/wiki/X86_Assembly
# - https://dman95.github.io/SASM/english.html 支持单步调试，用来看出错位置。
# - https://github.com/Fedjmike/mini-c/blob/master/cc.c
# - https://godbolt.org/
# - https://aaronbloomfield.github.io/pdr/book/x86-32bit-ccc-chapter.pdf
# - https://github.com/TinyCC/tinycc/blob/mob/tests/asmtest.S
# 约定，和系统和自己程序一致即可。
# - 变量类型只有 int，占 4 个字节。
# - 栈由高往低增长，栈顶指向。参数为正（+8,+12），局部变量（可选）为负（-4）。

LennaHammer

# FOR EACH TUPLE (x,z) IN RELATION b: 2 FOR EACH TUPLE (z,y) IN RELATION c: 3 IF (z) IN RELATION d: 4 ADD (x,y) TO RELATION a
# TODO: 否定
# 不实现，数学运算
data1 = [
  [:f, 1],
  [:f, 2],
  [:f, 3],
  [:g, 2],
  [:g, 3],
  [:':-', %i[h X], %i[f X], %i[g X]],

LennaHammer

class SexpParser
  def initialize
    @tokens = []
  end

  def parse_list
    xs = []
    xs << parse_atom until @tokens.fetch(0) == :')'
    @tokens.shift
    xs

LennaHammer

# Weakest Precondition
# 背景知识：Hoare Logic
# 这里最弱的意思是能从 require -> wp，比如wp要求是正数，而实际输入是大于10，即输入是wp的子集，wp的范围更大限制更松。
# wp可以针对不同语句根据规则生成
# 特别注意循环语句，根据所给的某一个正确的循环不变量来产生 wp。
# 考虑5种语句
# 1. 空语句 wp(SKIP,Q)=Q
# 2. 序列语句  wp(S1;S2, Q) = wp(S1, wp(S2,Q))
# 3. 赋值语句 wp(x=e, Q) = Q[e/x]
# 4. 条件语句 wp(IF B THEN S1 ELSE S2, Q) = ( B => wp(S1,Q) Λ !B => wp(S2,Q)) = (B Λ wp(S1, Q)) V (!B Λ wp(S2, Q))

LennaHammer

# https://github.com/taw/z3
# A Peer Architecture for Lightweight Symbolic Execution
require 'z3'
require 'ruby_parser'
parser = RubyParser.new
class Checker
  def initialize(eval_mode: true)
    @solver = Z3::Solver.new
    @eval_mode = eval_mode
  end

LennaHammer

单词表提取 (4912)

合计 4912 词，按词性和词频排列

[toc]

ADJ (662)

• good 好的 =agreeable : Okay, look, this is probably for the best, y'know? (145)