阿日哥的向量空间

Last time we defined the denotational semantics of IMP: In this lecture we’ll prove Kleene’s fixpoint theorem, which shows that the fixed point used to define the semantics of while commands exists, and work through examples of reasoning using the denotational semantics. Kleene’s Fixpoint Theorem Definition (Scott Continuity). A function from to is said to be Scott-continuous if for every chain we have It is not hard to show that if is Scott continuous, then it is also monotonic—that is, ...

We have now seen two operational models for programming languages: small-step and large-step. In this nnote, we consider a different semantic model, called denotational semantics. The idea in denotational semantics is to express the meaning of a program as the mathematical function that expresses what the program computes. We can think of an IMP program as a function from stores to stores: given an an initial store, the program produces a final store. For example, the program can be thought of ...

Equivalence of Semantics The small-step and large-step semantics are equivalent as captured by the following theorem. Theorem. For all commands and stores and we have The proof is left as an exercise. Non-Termination For a given command and initial state , the execution of the command may terminate with some final store , or it may diverge and never yield a final state. For example, the command always diverges while diverges if and only if the value of variable in the initial state is po ...

A Simple Imperative Language We will now consider a more realistic programming language, one where we can assign values to variables and execute control constructs such as if and while. The syntax for this imperative language, called IMP, is as follows: Small-step Operational Semantics We’ll first give a small-step operational semantics for IMP. The configurations in this language are of the form , , and , where is a store. The final configurations are of the form for commands, and for Bool ...

Large-Step Operational Semantics In the last lecture we defined a semantics for our language of arithmetic expressions using a small-step evaluation relation (and its reflexive and transitive closure ). In this note we will explore an alternative approach--large-step operational semantics--which yields the final result of evaluating an expression directly. Defining a large-step semantics boils down to specifying a relation that captures the evaluation of an expression. The relation has the fo ...

In this note, we will use the semantics of our simple language of arithmetic expressions, to express useful program properties, and we will prove these properties by induction. Program Properties There are a number of interesting questions about a language one can ask: Is it deterministic? Are there non-terminating programs? What sorts of errors can arise during evaluation? Having a formal semantics allows us to express these properties precisely. Determinism: Evaluation is deterministic, T ...

What is the meaning of a program? When we write a program, we represent it using sequences of characters. But these strings are just concrete syntax—they do not tell us what the program actually means. It is tempting to define meaning by executing programs--either using an interpreter or a compiler. But interpreters and compilers often have bugs! We could look in a specification manual. But such manuals typically only offer an informal description of language constructs. A better way to define m ...

准备环境 如果 docker 容器没有 vi 命令，可以自行安装： docker exec -it --user="root" es /bin/bashapt updateapt install 因为需要部署 kibana 容器，让 es和 kibana 容器互联，所以需要创建网络。 docker network create es-net 以安装 Elasticsearch 8.11.4 版本为例： docker pull elasticsearch:8.11。4 接下来创建挂载点目录： mkdir -p ~/apps/es/data ~/apps/es/config ~/apps/es/pluginschmod 777 ~/apps/es/datachmod 777 ~/apps/es/configchmod 777 ~/apps/es/plugins 部署单点es，创建es容器 执行以下命令： docker run -d \--restart=always \--name es \--network es-net \-p 9200:9200 \-p 9300:9300 \- ...

AArch64 is an ISA with a fixed instruction width of 32-bit. This obviously means there is not enough space to store a 64-bit immediate in a single instruction. Before working with AArch64 I was only familiar with x86 where this is a bit easier since instructions can have variable-width. A 64-bit immediate on x86-64 is really just the sequence of bytes: mov rax, 0x1122334455667788# encoded as: 0x48, 0xB8, 0x88, 0x77, 0x66, 0x55, 0x44, 0x33, 0x22, 0x11 A fixed-width ISA like ARM has to treat immed ...

支配结点 每个控制流图都一定有一个没有前驱的起始结点 ，这个结点是程序（或子程序）执行的假设开始点。 如果从 到结点 的所有有向边路径都经过结点 ，那么结点 是结点 的支配结点（或必经结点）， 支配 记作 。每一个结点都是自己的支配（必经）结点。 支配关系定理 在下文的引理中，默认 。 有向图的起点，亦是其所有结点的支配点； 定理 1：支配关系是自反的，反对称的，传递的。 自反性：显然，任意一个结点都是其自身的支配点。 传递性： 经过 的路径必定经过 ，经过 的路径必定经过 ，因此经过 的路径必定经过 ，即 。 反对称性： 假设 ，则任意一个到达 的路径都已经到达过 ，同时任意一个到达 的路径都已经到达过 ，矛盾。 定理 2： 在连通图中，若 ， 且 ，则有 或 。 证明： 考虑一条 的路径，若 ， 不存在支配关系，则一定存在一条不经过 的从 到 的路径，即存在一条 的路径，与 矛盾。 直接支配结点 我们将任意一个结点 的所有支配结点中，除自身外与自己距离最近的结点 称作 的直接支配点或直接必经结点（immediate dominator ...