交互设计中的问题:
- 尽量减少用户需要记忆的部分
- 缺乏反馈
本文主要内容来自 SpriCoder 的博客,更换了更清晰的图片并对原文的疏漏做了补充和修正。
交互框架
作用:
摘要
本文记述了 Ubuntu 22.04 中修改设备名称后导致 Microsoft Edge 浏览器因用户配置被锁定而不可用的问题及其解决方案。
在 Ubuntu 22.04 系统中突然无法从任务栏打开 Microsoft Edge 浏览器(表现为点击图表后鼠标开始转圈,但转圈结束后并没有响应)。
尝试在终端中打开 Microsoft Edge,遇到如下报错:
本文主要内容来自 SpriCoder 的博客,更换了更清晰的图片并根据新的课程设计做了补充和修正。
本文主要内容来自 SpriCoder 的博客,更换了更清晰的图片并根据新的课程设计做了补充和修正。

汽车上的刹车踏板和油门踏板相距很近,且刹车踏板要比油门踏板大很多:
设计学科通常借助模型生成新的想法并对其测试:如建筑学领域,有重量分布模型、空气环流模型、流体力学模型和光学模型等
交互设计领域:
SQL 编码为 FOL,基础理论,无代码;
SIGMOD2022 WeTune,王肇国等。
$$ \def\vis{\mathsf{\textcolor{orange}{vis}}} \def\ar{\mathsf{\textcolor{pink}{ar}}} \def\RW{\mathsf{RW}} \def\WW{\mathsf{\textcolor{red}{WW}}} \def\WR{\mathsf{\textcolor{blue}{WR}}} \def\visa{\xrightarrow{\vis}} \def\ara{\xrightarrow{\ar}} \def\RWa{\xrightarrow{\RW}} \def\WWa{\xrightarrow{\WW}} \def\WRa{\xrightarrow{\WR}} \def\wri{\mathsf{wri}} \def\Stmts{\mathtt{Stmts}} \def\IF{\mathtt{IF}} \def\true{\mathsf{true}} \def\AccID{\mathtt{AccID}} \def\ID{\mathtt{ID}} \def\bal{\mathtt{bal}} \def\Amount{\mathtt{Amount}} \def\Alive{\mathtt{Alive}} \def\Fields{\mathtt{Fields}} \def\T{\mathcal{T}} \def\R{\mathcal{R}} \def\D{\mathcal{D}} \def\V{\mathcal{V}} \def\bbT{\mathbb{T}} \def\bbV{\mathbb{V}} \def\bbZ{\mathbb{Z}} \def\B{\mathbb{B}} \def\v{\mathtt{v}} \def\f{\mathtt{f}} \def\FOREACH{\texttt{ FOREACH}} \def\IN{\texttt{ IN}} \def\DO{\texttt{ DO}} \def\END{\texttt{ END}} \def\NULL{\texttt{ NULL}} \def\Vars{\texttt{ Vars}} \def\LVar{\texttt{ LVar}} $$
摘要
尽管近年来开发了许多弱一致性机制来提高分布式复制系统的性能并确保可用性,但确保在此类系统上运行的事务应用程序的正确性仍然是一个困难而重要的问题。可串行化是事务性程序的一个众所周知的正确性标准; 然而,了解应用程序在弱一致性环境中执行时是否可序列化仍然是一项具有挑战性的工作。在这项工作中,我们结合了基于依赖图的可串行化特征,并利用抽象执行框架来开发一种全自动方法,用于在任何弱一致性模型下静态查找有界可串行化违规。我们将可序列化问题简化为一阶逻辑(FOL)中公式的可满足性问题,这使我们能够利用现有 SMT 求解器的功能。我们提供了从用 SQL 编写的程序(允许循环和条件)自动构造 FOL 编码的规则,并将一致性规范表示为 FOL 公式。除了检测有界可串行性违规之外,我们还提供了两种正交方案,通过提供充分的条件(同样以 FOL 公式的形式)来推理无界执行,其可满足性意味着在任何任意执行中都不存在异常。我们已将所提出的技术应用于 TPC-C(一个具有复杂应用程序逻辑的现实数据库程序),并且能够发现并行快照隔离(PSI)下的异常,并验证快照隔离(SI)下无限执行的可串行性,两个远弱于可串行化的一致性机制。
Nagar 与 Jagannathan 在本文中使用一阶谓词逻辑公式对客户程序以及事务一致性模型进行精确建模,利用 SAT/SMT 自动推导出违反该一致性的执行历史的结构,并在客户程序可能产生的所有执行历史中搜索该结构。
本文的工作是基于分布式数据一致性。
TODO:SQL 中的循环是否是必须的?
本文主要内容来自 SpriCoder 的博客,更换了更清晰的图片并根据新的课程设计做了补充和修正。
软件开发是一项既复杂又富有创造性的知识工作
软件开发——智力劳动: