Daniel's blog

Coq는 주로 소프트웨어와 수학적 증명의 형식적 검증에 사용되는 증명 도우미이다. 수학적 주장, 정의, 정리를 표현하기 위한 공식 언어와 이러한 주장에 대한 증명을 대화식으로 구성하고 검증하는 메커니즘을 제공한다. 전반적으로 Coq는 공식적인 추론과 검증을 위한 강력한 플랫폼을 제공하므로 소프트웨어 개발, 암호화, 안전이 중요한 시스템 등 정확성과 신뢰성이 중요한 영역에서 유용하게 사용할 수 있다. Coq의 주요 기능은 다음과 같다. 종속 유형 (Dependent Types): Coq는 귀납적 구조(Inductive Constructions)의 계산법이라는 유형 이론을 기반으로 한다(따라소 "COQ"라는 이름이 붙었다.). 유형이 용어에 종속되거나 그 반대의 경우도 허용하는 종속 유형을 지원한다. 이 기..

Factory Method Pattern은 객체 지향 프로그래밍에서 사용되는 창조적인 디자인 패턴이다. 이 패턴은 객체의 인스턴스화 프로세스를 서브 클래스에 위임하는 방법을 제공해 애플리케이션 아키텍처의 유연성을 높이고 분리할 수 있도록 한다. 이 패턴은 런타임까지 객체의 정확한 유형과 종속성을 확인할 수 없을 때 유용하다. 주요 개념Creator Classes: 객체를 생성하는 메서드를 선언하는 추상 클래스다. Factory Method 라고도 하는 이 메소드는 제품 클래스의 객체(product class)의 객체를 반환하기 위한 것이다.Concrete Creators: creator class를 상속하고 Factory Method를 재정의해 특정 product의 인스턴스를 반환하는 클래스다.Produ..

Nested Constructor는 일반적으로 클래스의 한 생성자가 같은 클래스의 다른 생성자를 호출해 초기화의 일부를 수행하는 디자인 패턴을 말한다. 이는 공통 초기화 로직을 단일 생성자에서 중앙 집중화하여 코드 중복을 줄이고 유지 관리성을 높이는 데 도움이 될 수 있다. 이 개념은 생성자 오버로딩을 지원하는 Java 및 C++과 같은 언어에서 가장 일반적으로 사용된다.  Java: Java에서 this() 를 사용해 같은 클래스 내에 다른 생성자를 호출할 수 있다. 'Car(String make, String model)' 생성자는 같은 클래스 내의 다른 생성자를 'this(make, model, 2020)'을 통해 호출할 수 있고 이는 'make'와 'model'을 재사용한다.public class..

Queue와 Thread라는 용어는 프로그래밍에서 일반적으로 멀티태스킹 및 동시 실행과 관련된 별개의 개념을 나타낸다. 성능과 효율성이 중요한 환경에서 효과적인 프로그래밍을 위해서는 아래 개념을 이해하는 것이 중요하다. Queue개념: Queue는 데이터를 선입선출(FIFO) 방식으로 저장하고 관리하는 데 사용되는 데이터 구조다. 대기열에 가장 먼저 추가된 항목이 가장 먼저 제거된다. 이는 사람들이 줄을 서는 것과 비슷하며, 가장 먼저 줄을 선 사람이 가장 먼저 서비스를 받는 것과 비슷하다.사용법: Queue는 프로그래밍에서 작업, 데이터 처리 또는 이벤트를 순차적으로 처리하기 위해 자주 사용된다. 또한 데이터를 처리하기 전에 일시적으로 보관하는 버퍼링을 관하는 데에도 사용할 수 있다.유형: Linear..

Rabin-Karp Algorithm은 hasing을 사용해 텍스트의 패턴 문자열 집합 중 중 하나를 찾는 문자열 검색 알고리즘이다. 1987년 마이클 라빈(Michael Rabin)과 Richard Karp(리차드 카프)가 개발했다. 이 알고리즘의 핵심 아이디어는 검색하려는 패턴의 해시값을 계산한 다음 이 해시를 패턴과 길이가 같은 텍스트의 하위 문자열의 해시값과 비교하는 것이다. 이 방법을 사용하면 패턴과 일치할 가능성이 없는 텍스트의 많은 부분을 빠르게 건너뛸 수 있기 때문에 특히 패턴이 텍스트보다 훨씬 작은 경우 검색의 속도를 크게 높일 수 있다. 알고리즘의 개요는 아래와 같다. 해시 함수 : 각 문자열을 숫자 값으로 변환하는 해시 함수를 선택한다. 초기 해시 값 : 길이가 m인 패턴 P의 해시값..

이진 트리 또는 이진 검색 트리(BST)에서 두 노드의 최하 공통 조상(LCA)를 찾는 데는 몇 가지 일반적인 접근 방식이 있다. 가장 좋은 방법은 트리이 특정 특성(BST 인지, 균형이 잡혀있는지(balanced) 등)과 추가 정보 (각 노드의 조상 또는 트리의 전처리 기능 등)에 따라 달라진다. 아래는 몇 가지 일반적인 방법이다. Single Traveral Method (단일 순회 방법, 재귀 사용) : 이 방법은 추가 정보가 제공되지 않는 트리에서 LCA를 찾는 데 널리 사용되는 방법이다. 아이디어 : 루트에서 시작해 트리를 순회한다. 각 노드에 대해 현재 노드가 LCA를 찾고자 하는 두 노드 중 하나인지 확인한다. 맞다면 현재 노드를 반환한다. 그렇지 않으면 왼쪽 및 오른쪽 자식에 대해 재귀 호..

에라토스테네스의 체는 소수를 찾아내기 위한 알고리즘으로, 교과 과정에서도 배우는 내용 중 하나다. 이 알고리즘은 LeetCode 204. Count Primes 와 같은 인터뷰에도 종종 등장하므로 알고 있으면 매우 유용하다. 고대 그리스 수학자 에라토스테네스가 발견한 이 알고리즘은 '체'로 치듯이 수를 걸러낸다고 해 '에라토스테네스의 체'로 불린다. 이 알고리즘의 포인트는 배수와 제곱근을 활용하는 것이다. 예를 통해 이해해보자. 1부터 100까지의 숫자 중 소수를 찾는다 가정하자. 1부터 100까지의 숫자를 나열해보자. 작은 숫자부터 시작을 하고, 특수한 경우인 1을 우선 지운다. 2를 제외한 2의 배수를 지운다. (배수 활용 시작) 3을 제외한 3의 배수를 지운다. 4의 배수는 이미 2의 배수를 통해 ..

Adaptive Beamforming은 레디어 시스템, 무선 통신 시스템, 소나 (수중 음파 탐지) 등의 센서 배열에서 신호의 수신 또는 전송을 특정 방향으로 유도하기 위해 사용되는 고급 신호 처리 기술이다. 신호 빔의 방향성을 동적으로 조정해 다른 신호의 간섭을 최소화하면서 원하는 신호에 더 집중할 수 있다. Adaptive Beamforming은 다양한 적용에서 신호 품질과 방향성을 향상시키는 데 중요한 역할을 하며 최신 통신 및 감지 시스템의 핵심 기술로 자리 잡고 있다. 파티에서 대화하는 상황을 빗대 이해를 해보자. 손님들로 가득 찬 시끄러운 파티에서 친구의 이야기를 듣고 싶다고 상상해 보자. 친구는 방 한 구석에 있고 음악이 흘러나오고 있으며 주변에서는 여러 가지 대화가 오가고 있다. 친구의 이..

Checksum은 전송 또는 저장 중에 발생할 수 있는 오류를 감지하기 위해 디지털 테이블 블록에서 파생된 작은 크기의 데이터다. 기본 개념은 메시지나 파일의 내용을 기반으로 값(Checksum)을 계산한 다음 이 값을 사용해 나중에 데이터의 무결성(integrity)를 검증하는 것이다. 이 프로세스에는 데이터의 표현 역할을 하는 짧은 고정 길이 값(Checksum)을 생성하는 알고리즘을 데이터에서 실행하는 것이 포함된다. 나중에 데이터를 검색하거나 수신하면 Checksum 계산이 반복된다. 새로 계산된 Checksum이 원래 Checksum과 일치하면 일반적으로 데이터가 변경되지 않은 것으로 간주하지만, 의도적인 변조를 방지할 수 있는 것은 아니다. Checksum이 일치하지 않으면 데이터가 어떤 식으..

1. Stack 정의 : stack은 로컬 변수, 함수 매개변수, 반환 주소를 저장하는 메모리 영역으로, 함수 호출 관리를 수행한다. 관리 : stack은 시스템에 의해 자동으로 관리된다. 함수가 호출되면 해당 함수의 로컬 변수, 반환 주소 및 일부 관리 정보가 stack에 push된다. 함수가 반환되면 해당 정보가 stack에서 pop된다. LIFO 구조 : stack은 Last-In-First-Out (LIFO) 방식으로 작동한다. 이는 stack에 마지막으로 push 된 변수가 제일 먼저 제거된다는 의미다. 크기 : stack에는 프로그램 시작 시 설정된 제한된 크기가 있다. 사용 가능한 스택 공가보다 더 많은 공간을 사용하면 (예를 들어, 무한 재귀로 인한) stack overflow가 발생하며 ..