|
我支持Pebble Time kickstarter活动，首先成为酷孩子的一部分，并尝试在设备上进行一些Ada黑客攻击。 
故事 当Pebble Time kickstarter穿过屋顶时，我看了一下规格并发现手表在STM32F4上运行，这是一个由GNAT支持的ARM cortex-M4 CPU。所以我支持这个活动，首先成为酷孩子的一部分，并尝试一些Ada黑客入侵设备。 起初我不确定我是要完全替换Pebble OS还是仅为它编写应用程序。第一个选项需要重新编写所有驱动程序（屏幕，蓝牙等），我还需要一种编程芯片的方法，据我所知，需要打开手表并将调试接口焊接到芯片上。由于我还没准备好为了黑客而打开200美元的手表，我决定选择第二个选项，编写应用程序。 将C API绑定到Ada Pebble SDK经过深思熟虑，提供了一个基于QEMU的仿真器，非常适合测试。事实上，在我得到真正的手表之前，我开发并测试了这个SDK的绑定。 整个API包含在一个C头（pebble.h）中。我使用GNAT的switch -fdump-ada-spec生成绑定的第一个版本，然后我重新格式化它以拆分包中的功能并重命名子程序。例如，函数layer_create变为： package ; API几乎只使用指向隐藏结构的指针： typedef Window *window_create( 我们可以方便地在Ada中映射如下： 总的来说，绑定相对容易创建。 Smartwatch应用程序和正式证明 为了使用这种绑定，我决定移植由Yannick和Tristan在SPARK中编写的正式证明的俄罗斯方块。 游戏系统是相同的，这个端口包括一个新的图形前端，菜单和按钮处理。该应用程序非常简单易用，Pebble API设计精良且易于使用。 正式的证明集中在那些无法测试的东西上，在我们的例子中，就是游戏系统。您能想出一种方法来测试代码是否会拒绝任何部分、任何方向、任何位置以及任何可能的电路板板状态(即数万亿或千万亿的组合)上的无效移动吗? 我们从SPARK分析得到的第一件事是没有运行时错误。例如，对我们来说，这意味着我们肯定不会对游戏板矩阵进行无效访问。 然后我们证明高级的游戏属性，如： 切勿将落下的部件移动到无效位置 落下的部件永远不会与板上已有的部件重叠 删除所有完整的行 无论玩家做什么，游戏总是处于有效状态 此应用程序在Pebble应用程序商店以PATRIS 的名义发布，截至目前已有超过660位用户下载了它。 我还使用块来制作表盘来显示时间数字。 持久存储 我做的最后一件事是创建一个更高的持久存储API接口，一种存储数据的机制，并在关闭应用程序后检索它。 C接口非常简单，只有几个功能。每个数据都与uint32_t键相关联，因此应用程序可以读取，写入和测试给定键的数据是否存在。 int int bool 但是，Ada类型系统不喜欢void指针，并且能够使用持久存储而不必处理令人讨厌的未经检查的转换（与C强制转换相同）我编写了一个自动处理所有内容的通用包： generic Data_Key : Uint32_T; package -- Write data associated with the key, return True on success -- Read data associated with the key, return True on success -- Return True if there is data associated with the key -- Erase data associated with the key end 使用持久存储现在很简单： Level : Natural; XP : Natural; Player : My_Data; begin Player.XP := 0; Player.Level := 1; -- Insert complex gameplay here… Put_Line ("The game could not be saved"); 来源 绑定和应用程序源代码可在GitHub上获得。 代码 Ada_Time Fabien-Chouteau / Ada_Time Ada绑定Pebble Time智能手表 相关文件---
Ada_Time-master.zip
(131.54 KB, 下载次数: 0)
|
微信公众号
手机版
