EagleBear2002 的博客

这里必须根绝一切犹豫,这里任何怯懦都无济于事

摘要

本文记述了 Ubuntu 22.04 中修改设备名称后导致 Microsoft Edge 浏览器因用户配置被锁定而不可用的问题及其解决方案。

问题描述

在 Ubuntu 22.04 系统中突然无法从任务栏打开 Microsoft Edge 浏览器(表现为点击图表后鼠标开始转圈,但转圈结束后并没有响应)。

尝试在终端中打开 Microsoft Edge,遇到如下报错:

阅读全文 »

本文主要内容来自 SpriCoder 的博客,更换了更清晰的图片并根据新的课程设计做了补充和修正。

人机交互的发展历史

  1. 新的界面变革包含了上一代界面:作为一种特例
  2. 旧的交互方式仍有其存在的必要性:以前的用户从未消失
  3. 学习目的:利用原有技术实现新的交互手段

重要的学术事件

  1. 1945 年,Vannevar Bush,“As we may think”(诚如所思):应借助设备或技术帮助科学家检索、记录、分析及传输各种信息,Memex 工作站
  2. 1959 年,HCI 领域第一篇论文:从减轻操作疲劳的角度讨论计算机控制台设计
  3. 1960 年
    1. JCR Licklider 提出“Human-Computer Symbiosis”(人机共生)
    2. HCI 的启蒙观点
  4. HCI 的里程碑:1969 年,第一次人机系统国际大会召开,第一份专业杂志创刊
  5. 1970 年,英国拉夫堡(Loughbocough)大学的 HUSAT 研究中心和 Xerox 公司的 Palo Alto 研究中心成立(PARC)
  6. 1980s,出版学术专著,Interface->Interaction
  7. 1990s,智能化交互、多通道交互、虚拟现实、脑机交互
阅读全文 »

本文主要内容来自 SpriCoder 的博客,更换了更清晰的图片并根据新的课程设计做了补充和修正。

背景

  1. 观察用户怎样工作是极其重要的可用性方法
    1. 用户并不总能客观和完整地描述产品的使用情况:访谈得到的信息可能不真实
    2. 用户有可能忽略一些细节:忽视了细节的重要性
    3. Heath 和 Luff 在伦敦地铁控制室的观察证明有助于改进系统设计
  2. 观察法是所有可用性方法中最简单的方法:涉及看和听两个方面
  3. 观察适用于产品开发的任何阶段
    1. 初期:理解用户的需要
    2. 开发过程:检查原型
    3. 后期:对最终产品进行评价

观察方法

阅读全文 »

背景

汽车上的刹车踏板和油门踏板相距很近,且刹车踏板要比油门踏板大很多:

  1. 经验告诉我们,可达到以最快的速度准确制动的目的
  2. 但是,依据的原理是什么呢?

设计学科通常借助模型生成新的想法并对其测试:如建筑学领域,有重量分布模型、空气环流模型、流体力学模型和光学模型等

交互设计领域:

阅读全文 »

摘要

本文推荐了一些程序员实用软件,包括装机软件和效率软件,全部为免费软件,并提供了获取方式。

本文所提供的一切软件服务获取方式仅供教学科研使用!

装机软件

微软办公

阅读全文 »

CONCUR'18 Anode[^Kartik]

SQL 编码为 FOL,基础理论,无代码;

SIGMOD'22 WeTune[^WeTune]

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 的博客,更换了更清晰的图片并根据新的课程设计做了补充和修正。

【2014】自主团队

【2013】【2015A】【2016】软件开发是知识工作

软件开发是一项既复杂又富有创造性的知识工作

软件开发——智力劳动:

阅读全文 »