Портирование Android-приложений в экосистему HarmonyOS NEXT с использованием формальных спецификаций

HarmonyOS изначально была разработана на основе AOSP и поддерживала запуск Android-приложений, однако после масштабного обновления до HarmonyOS NEXT эта совместимость стала недоступной, и Android-приложения больше не могут работать на платформе напрямую. Это привело к необходимости переносить приложения в нативную среду HarmonyOS NEXT, что стало серьезной проблемой для наполнения экосистемы.

Расскажу про один из способов автоматизированного портирования Android-приложений под HarmonyOS NEXT с сохранением архитектуры и семантики программы. В основе подхода — преобразование исходного Kotlin-кода в ArkTS. Для анализа проекта используется Kotlin PSI, на основе которого строится промежуточное представление, после чего генерируется целевой код. Также в докладе будет уделено внимание портированию пользовательского интерфейса, где будут описаны способы трансляции декларативного UI фреймворка Jetpack Compose в ArkUI.

Отдельная сложность портирования связана с вызовами библиотек: в коде Android-приложений используются функции и классы из стандартной библиотеки Kotlin и Android SDK, которые не имеют прямых аналогов в HarmonyOS NEXT. Поэтому простая синтаксическая замена вызовов невозможна — требуется установить семантическое соответствие API двух платформ. В отличие от языка, чья семантика задается конечным набором конструкций и может быть полностью покрыта правилами трансляции, множество библиотечных API практически неограниченно, из-за чего требуется механизм автоматического сопоставления поведения. Для решения этой проблемы используется подход на основе формальных спецификаций, где поведение библиотечных функций описывается в виде предусловий, постусловий и действий, а совместимость исходных и целевых вызовов проверяется с применением SMT-решателя. Это позволяет автоматически подбирать эквивалентные цепочки вызовов на стороне HarmonyOS NEXT и сохранять семантику приложения при переносе.

Целевая аудитория доклада — разработчики и инженеры, интересующиеся новыми мобильными платформами, а также верификацией ПО, формальными спецификациями и трансляцией программных компонентов.